case pos
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ∀ (x : G), x ∈ H → x = 1
⊢ H = ⊥ ∨ Nontrivial { x // x ∈ H }

case neg
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ¬∀ (x : G), x ∈ H → x = 1
⊢ H = ⊥ ∨ Nontrivial { x // x ∈ H }
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial { x // x ∈ H }
by_cases h : ∀ x ∈ H, x = (1 : G)
case pos.h
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ∀ (x : G), x ∈ H → x = 1
⊢ H = ⊥
case pos
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ∀ (x : G), x ∈ H → x = 1
⊢ H = ⊥ ∨ Nontrivial { x // x ∈ H }
left
no goals
case pos.h
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ∀ (x : G), x ∈ H → x = 1
⊢ H = ⊥
exact H.eq_bot_iff_forall.mpr h
case neg.h
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ¬∀ (x : G), x ∈ H → x = 1
⊢ Nontrivial { x // x ∈ H }
case neg
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ¬∀ (x : G), x ∈ H → x = 1
⊢ H = ⊥ ∨ Nontrivial { x // x ∈ H }
right
case neg.h
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ∃ x x_1, ¬x = 1
⊢ Nontrivial { x // x ∈ H }
case neg.h
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ¬∀ (x : G), x ∈ H → x = 1
⊢ Nontrivial { x // x ∈ H }
simp only [not_forall] at h
no goals
case neg.h
G : Type u_1
G' : Type ?u.174621
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.174630
inst✝ : AddGroup A
H✝ K H : Subgroup G
h : ∃ x x_1, ¬x = 1
⊢ Nontrivial { x // x ∈ H }
simpa [nontrivial_iff_exists_ne_one] using h