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

State before:
α : Type ?u.5373
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
⊢ K < K' ↔ map f K < map f K'
Tactic:
simp only [lt_iff_le_not_le]
State after:
α : Type ?u.5373
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
⊢ K ≤ K' ∧ ¬K' ≤ K ↔ map f K ≤ map f K' ∧ ¬map f K' ≤ map f K

State before:
α : Type ?u.5373
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
⊢ K ≤ K' ∧ ¬K' ≤ K ↔ map f K ≤ map f K' ∧ ¬map f K' ≤ map f K
Tactic:
simp_rw [← Subgroup.map_iff_mono_of_injective hf]
State after:
no goals