G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
⊢ ⊤ ≤ map f ⊤
G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
⊢ map f ⊤ = ⊤
rw [eq_top_iff]
G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ map f ⊤
G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
⊢ ⊤ ≤ map f ⊤
intro x _
case intro
G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
x : N
a✝ : x ∈ ⊤
y : G
hy : ↑f y = x
⊢ x ∈ map f ⊤
G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ map f ⊤
obtain ⟨y, hy⟩ := h x
no goals
case intro
G : Type u_1
G' : Type ?u.282904
inst✝⁴ : Group G
inst✝³ : Group G'
A : Type ?u.282913
inst✝² : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_2
inst✝¹ : Group N
P : Type ?u.282940
inst✝ : Group P
f : G →* N
h : Surjective ↑f
x : N
a✝ : x ∈ ⊤
y : G
hy : ↑f y = x
⊢ x ∈ map f ⊤
exact ⟨y, trivial, hy⟩