[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ IsSemiringHom _root_.id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x + y) = _root_.id x + _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x * y) = _root_.id x * _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ + y✝) = _root_.id x✝ + _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_4
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf : IsSemiringHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ * y✝) = _root_.id x✝ * _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
⊢ (g ∘ f) 0 = 0
[PROOFSTEP]
simpa [map_zero hf] using map_zero hg
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
⊢ (g ∘ f) 1 = 1
[PROOFSTEP]
simpa [map_one hf] using map_one hg
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x✝ y✝ : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
x y : α
⊢ (g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
[PROOFSTEP]
simp [map_add hf, map_add hg]
[GOAL]
α : Type u
β : Type v
inst✝² : Semiring α
inst✝¹ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x✝ y✝ : α
hf : IsSemiringHom f
γ : Type u_1
inst✝ : Semiring γ
g : β → γ
hg : IsSemiringHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
[PROOFSTEP]
simp [map_mul hf, map_mul hg]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
src✝ : IsSemiringHom f := hf
⊢ ∀ (x y : α), f (x + y) = f x + f y
[PROOFSTEP]
apply @‹IsSemiringHom f›.map_add
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f 0 = f (0 + 0) - f 0
[PROOFSTEP]
rw [hf.map_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f 0 = f 0 + f 0 - f 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (0 + 0) - f 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (-x) = f (-x + x) - f x
[PROOFSTEP]
rw [hf.map_add]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (-x) = f (-x) + f x - f x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (-x + x) - f x = -f x
[PROOFSTEP]
simp [hf.map_zero]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
⊢ f (x - y) = f x - f y
[PROOFSTEP]
simp [sub_eq_add_neg, hf.map_add, hf.map_neg]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ IsRingHom _root_.id
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x * y) = _root_.id x * _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ ∀ (x y : α), _root_.id (x + y) = _root_.id x + _root_.id y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y : α
⊢ _root_.id 1 = 1
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ * y✝) = _root_.id x✝ * _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3
α : Type u
β : Type v
inst✝¹ : Ring α
inst✝ : Ring β
f : α → β
hf : IsRingHom f
x y x✝ y✝ : α
⊢ _root_.id (x✝ + y✝) = _root_.id x✝ + _root_.id y✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ (g ∘ f) 1 = 1
[PROOFSTEP]
simp [map_one hf]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x y : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
⊢ g 1 = 1
[PROOFSTEP]
exact map_one hg
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
[PROOFSTEP]
simp [map_mul hf]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x * f y) = g (f x) * g (f y)
[PROOFSTEP]
rw [map_mul hg]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ (g ∘ f) (x + y) = (g ∘ f) x + (g ∘ f) y
[PROOFSTEP]
simp [map_add hf]
[GOAL]
α : Type u
β : Type v
inst✝² : Ring α
inst✝¹ : Ring β
f : α → β
hf✝ : IsRingHom f
x✝ y✝ : α
hf : IsRingHom f
γ : Type u_1
inst✝ : Ring γ
g : β → γ
hg : IsRingHom g
x y : α
⊢ g (f x + f y) = g (f x) + g (f y)
[PROOFSTEP]
rw [map_add hg]
