case h.e'_2.a
G : Type u_1
G' : Type ?u.178833
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.178842
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ (∃ x, x ∈ H ∧ x ≠ 1) ↔ Nontrivial { x // x ∈ H }
G : Type u_1
G' : Type ?u.178833
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.178842
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ H = ⊥ ∨ ∃ x, x ∈ H ∧ x ≠ 1
convert H.bot_or_nontrivial
no goals
case h.e'_2.a
G : Type u_1
G' : Type ?u.178833
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.178842
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ (∃ x, x ∈ H ∧ x ≠ 1) ↔ Nontrivial { x // x ∈ H }
rw [nontrivial_iff_exists_ne_one]