no goals
α : Type ?u.229687
β : Type ?u.229690
M : Type ?u.229693
N : Type ?u.229696
P : Type ?u.229699
G✝ : Type ?u.229702
H✝ : Type ?u.229705
F : Type u_3
inst✝⁴ : Group G✝
inst✝³ : CommGroup H✝
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : MulOneClass H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), ↑f a = 1 → a = 1
x y : G
hxy : ↑f x = ↑f y
⊢ ↑f (x * y⁻¹) = 1
rw [map_mul, hxy, ← map_mul, mul_inv_self, map_one]