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

State before:
α : Type ?u.7056
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K = map f K' ↔ K = K'
Tactic:
simp only [le_antisymm_iff, ← Subgroup.map_iff_mono_of_injective hf]
State after:
no goals