G : Type u_1
H : Type u_2
A : Type ?u.69287
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)⁻¹ = 1
⊢ f a = f b
G : Type u_1
H : Type u_2
A : Type ?u.69287
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f (a * b⁻¹) = 1
⊢ f a = f b
rw [hf.map_mul, hf.map_inv] at h
no goals
G : Type u_1
H : Type u_2
A : Type ?u.69287
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)⁻¹ = 1
⊢ f a = f b
rw [← inv_inv (f b), eq_inv_of_mul_eq_one_left h]