Theorem: Subgroup.map_subgroupOf_eq (Jordan/AlternatingMaximal.lean)

State before:
α : Type ?u.335
G : Type u_1
H : Type ?u.341
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
K : Subgroup ↥N
⊢ subgroupOf (map (Subgroup.subtype N) K) N = K
Tactic:
rw [← Subgroup.comap_subtype, Subgroup.comap_map_eq, Subgroup.ker_subtype, sup_bot_eq]
State after:
no goals