G : Type u_1
H : Type u_2
A : Type ?u.71750
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.71750
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
case a
G : Type u_1
H : Type u_2
A : Type ?u.71750
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.71750
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
apply inv_injective
no goals
case a
G : Type u_1
H : Type u_2
A : Type ?u.71750
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 [eq_inv_of_mul_eq_one_left h]