no goals
G : Type u_1
H : Type ?u.121913
A : Type ?u.121916
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s t : Set G
ht : IsSubgroup t
h : s ⊆ t
a : G
ha : a ∈ closure s
⊢ a ∈ t
induction ha <;> simp [h _, *, ht.one_mem, ht.mul_mem, IsSubgroup.inv_mem_iff]