case h
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
⊢ ∀ (a : Subgroup G), a < ⊤ → a < normalizer a ↔ normalizer a = a → a = ⊤
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), normalizer H = H → H = ⊤
apply forall_congr'
case h
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H✝ K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
H : Subgroup G
⊢ H < ⊤ → H < normalizer H ↔ normalizer H = H → H = ⊤
case h
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
⊢ ∀ (a : Subgroup G), a < ⊤ → a < normalizer a ↔ normalizer a = a → a = ⊤
intro H
case h
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H✝ K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
H : Subgroup G
⊢ ¬H = ⊤ → ¬H = normalizer H ↔ normalizer H = H → H = ⊤
case h
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H✝ K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
H : Subgroup G
⊢ H < ⊤ → H < normalizer H ↔ normalizer H = H → H = ⊤
simp only [lt_iff_le_and_ne, le_normalizer, true_and_iff, le_top, Ne.def]
no goals
case h
G : Type u_1
G' : Type ?u.405590
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.405599
inst✝¹ : AddGroup A
H✝ K : Subgroup G
N : Type ?u.405617
inst✝ : Group N
H : Subgroup G
⊢ ¬H = ⊤ → ¬H = normalizer H ↔ normalizer H = H → H = ⊤
tauto