M : Type u_1
N : Type ?u.25831
A : Type ?u.25834
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
this : ∀ (x : M), x ∈ closure s → p x
⊢ p x
M : Type u_1
N : Type ?u.25831
A : Type ?u.25834
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p x
have : ∀ x ∈ closure s, p x := fun x hx => closure_induction hx Hs H1 Hmul
no goals
M : Type u_1
N : Type ?u.25831
A : Type ?u.25834
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
H1 : p 1
Hmul : ∀ (x y : M), p x → p y → p (x * y)
this : ∀ (x : M), x ∈ closure s → p x
⊢ p x
simpa [hs] using this x