G : Type u_1
G' : Type ?u.170709
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.170718
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ (∃ y x, y ≠ ↑1) ↔ ∃ x, x ∈ H ∧ x ≠ 1
G : Type u_1
G' : Type ?u.170709
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.170718
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ Nontrivial { x // x ∈ H } ↔ ∃ x, x ∈ H ∧ x ≠ 1
rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
no goals
G : Type u_1
G' : Type ?u.170709
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.170718
inst✝ : AddGroup A
H✝ K H : Subgroup G
⊢ (∃ y x, y ≠ ↑1) ↔ ∃ x, x ∈ H ∧ x ≠ 1
simp