[GOAL]
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
⊢ H = ⊥ ∨ H = ⊤
[PROOFSTEP]
refine' (iH.comap f).eq_bot_or_eq_top.imp (fun h => _) fun h => _
[GOAL]
case refine'_1
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
h : comap f H = ⊥
⊢ H = ⊥
[PROOFSTEP]
rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
[GOAL]
case refine'_2
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
h : comap f H = ⊤
⊢ H = ⊤
[PROOFSTEP]
rw [← comap_top f] at h 
[GOAL]
case refine'_2
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ↑f
H : Subgroup H✝
iH : Normal H
h : comap f H = comap f ⊤
⊢ H = ⊤
[PROOFSTEP]
exact comap_injective hf h
