no goals
M : Type u_1
inst✝¹ : Monoid M
s✝ : Set M
A : Type ?u.62775
inst✝ : AddMonoid A
t✝ : Set A
s t : Set M
ht : IsSubmonoid t
h : s ⊆ t
a : M
ha : a ∈ Closure s
⊢ a ∈ t
induction ha <;> simp [h _, *, IsSubmonoid.one_mem, IsSubmonoid.mul_mem]