G : Type u_1
H : Type ?u.34551
A : Type ?u.34554
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
⊢ (∀ (x : G), x ∈ s ↔ x = 1) ↔ ∀ (x : G), x ∈ s → x = 1
G : Type u_1
H : Type ?u.34551
A : Type ?u.34554
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
⊢ s = trivial G ↔ ∀ (x : G), x ∈ s → x = 1
simp only [Set.ext_iff, IsSubgroup.mem_trivial]
no goals
G : Type u_1
H : Type ?u.34551
A : Type ?u.34554
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
⊢ (∀ (x : G), x ∈ s ↔ x = 1) ↔ ∀ (x : G), x ∈ s → x = 1
exact ⟨fun h x => (h x).1, fun h x => ⟨h x, fun hx => hx.symm ▸ hs.toIsSubmonoid.one_mem⟩⟩