[GOAL]
α : Type u
β : Type v
inst✝² : Mul α
inst✝¹ : Mul β
γ : Type u_1
inst✝ : Mul γ
f : α → β
g : β → γ
hf : IsMulHom f
hg : IsMulHom g
x y : α
⊢ (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
[PROOFSTEP]
simp only [Function.comp, hf.map_mul, hg.map_mul]
[GOAL]
α✝ : Type u
β✝ : Type v
inst✝⁴ : Mul α✝
inst✝³ : Mul β✝
γ : Type u_1
inst✝² : Mul γ
α : Type u_2
β : Type u_3
inst✝¹ : Semigroup α
inst✝ : CommSemigroup β
f g : α → β
hf : IsMulHom f
hg : IsMulHom g
a b : α
⊢ f (a * b) * g (a * b) = f a * g a * (f b * g b)
[PROOFSTEP]
simp only [hf.map_mul, hg.map_mul, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
α : Type u
β : Type v
inst✝¹ : MulOneClass α
inst✝ : Group β
f : α → β
hf : IsMulHom f
⊢ ?m.13736 hf * f 1 = ?m.13736 hf
[PROOFSTEP]
rw [← hf.map_mul, one_mul]
[GOAL]
α : Type u
β : Type v
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
f : α → β
hf : IsMonoidHom f
γ : Type u_1
inst✝ : MulOneClass γ
g : β → γ
hg : IsMonoidHom g
src✝ : IsMulHom (g ∘ f) := IsMulHom.comp hf.toIsMulHom hg.toIsMulHom
⊢ g (f 1) = 1
[PROOFSTEP]
rw [hf.map_one, hg.map_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f : α → β
hf✝ hf : IsGroupHom f
a : α
⊢ f a⁻¹ * f a = 1
[PROOFSTEP]
rw [← hf.map_mul, inv_mul_self, hf.map_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f : α → β
hf✝ hf : IsGroupHom f
a b : α
⊢ f (a / b) = f a / f b
[PROOFSTEP]
simp_rw [div_eq_mul_inv, hf.map_mul, hf.map_inv]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f✝ : α → β
hf✝ : IsGroupHom f✝
f : α → β
hf : IsGroupHom f
h : Function.Injective f
x✝ : α
⊢ f x✝ = 1 → x✝ = 1
[PROOFSTEP]
rw [← hf.map_one]
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f✝ : α → β
hf✝ : IsGroupHom f✝
f : α → β
hf : IsGroupHom f
h : Function.Injective f
x✝ : α
⊢ f x✝ = f 1 → x✝ = 1
[PROOFSTEP]
exact @h _ _
[GOAL]
α : Type u
β : Type v
inst✝¹ : Group α
inst✝ : Group β
f✝ : α → β
hf✝ : IsGroupHom f✝
f : α → β
hf : IsGroupHom f
h : ∀ (a : α), f a = 1 → a = 1
x y : α
hxy : f x = f y
⊢ f (x / y) = 1
[PROOFSTEP]
rwa [hf.map_div, div_eq_one]
[GOAL]
α✝ : Type u
β✝ : Type v
α : Type u_1
β : Type u_2
inst✝¹ : AddGroup α
inst✝ : AddCommGroup β
f g : α → β
hf : IsAddGroupHom f
hg : IsAddGroupHom g
⊢ IsAddGroupHom fun a => f a - g a
[PROOFSTEP]
simpa only [sub_eq_add_neg] using hf.add hg.neg
