case mp
G : Type u_1
G' : Type ?u.513580
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.513589
inst✝³ : AddGroup A
N : Type ?u.513595
P : Type ?u.513598
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_2
inst✝ : MulOneClass M
f : G →* M
x y : G
h : ↑f x = ↑f y
⊢ y⁻¹ * x ∈ ker f

case mpr
G : Type u_1
G' : Type ?u.513580
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.513589
inst✝³ : AddGroup A
N : Type ?u.513595
P : Type ?u.513598
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_2
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ ker f
⊢ ↑f x = ↑f y
G : Type u_1
G' : Type ?u.513580
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.513589
inst✝³ : AddGroup A
N : Type ?u.513595
P : Type ?u.513598
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_2
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ ↑f x = ↑f y ↔ y⁻¹ * x ∈ ker f
constructor <;> intro h
no goals
case mp
G : Type u_1
G' : Type ?u.513580
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.513589
inst✝³ : AddGroup A
N : Type ?u.513595
P : Type ?u.513598
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_2
inst✝ : MulOneClass M
f : G →* M
x y : G
h : ↑f x = ↑f y
⊢ y⁻¹ * x ∈ ker f
rw [mem_ker, map_mul, h, ← map_mul, inv_mul_self, map_one]
no goals
case mpr
G : Type u_1
G' : Type ?u.513580
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.513589
inst✝³ : AddGroup A
N : Type ?u.513595
P : Type ?u.513598
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_2
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ ker f
⊢ ↑f x = ↑f y
rw [← one_mul x, ← mul_inv_self y, mul_assoc, map_mul, f.mem_ker.1 h, mul_one]