G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ ker f
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) = H ⊔ ker f
refine' le_antisymm _ (sup_le (le_comap_map _ _) (ker_le_comap _ _))
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ ker f
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ ker f
intro x hx
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x
⊢ x ∈ H ⊔ ker f
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ ker f
simp only [exists_prop, mem_map, mem_comap] at hx
case intro.intro
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : ↑f y = ↑f x
⊢ x ∈ H ⊔ ker f
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x
⊢ x ∈ H ⊔ ker f
rcases hx with ⟨y, hy, hy'⟩
case intro.intro
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : ↑f y = ↑f x
⊢ y * (y⁻¹ * x) ∈ H ⊔ ker f
case intro.intro
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : ↑f y = ↑f x
⊢ x ∈ H ⊔ ker f
rw [← mul_inv_cancel_left y x]
no goals
case intro.intro
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : ↑f y = ↑f x
⊢ y * (y⁻¹ * x) ∈ H ⊔ ker f
exact mul_mem_sup hy (by simp [mem_ker, hy'])
no goals
G : Type u_1
G' : Type ?u.565766
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.565775
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f : G →* N
H : Subgroup G
x y : G
hy : y ∈ H
hy' : ↑f y = ↑f x
⊢ y⁻¹ * x ∈ ker f
simp [mem_ker, hy']