G : Type u_1
H : Type u_2
A : Type ?u.74216
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
this : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 1
G : Type u_1
H : Type u_2
A : Type ?u.74216
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
⊢ f (a * b⁻¹) = 1
have : f a * (f b)⁻¹ = 1 := by rw [h, mul_right_inv]
no goals
G : Type u_1
H : Type u_2
A : Type ?u.74216
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
this : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 1
rwa [← hf.map_inv, ← hf.map_mul] at this
no goals
G : Type u_1
H : Type u_2
A : Type ?u.74216
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
⊢ f a * (f b)⁻¹ = 1
rw [h, mul_right_inv]