M : Type u_1
N : Type ?u.18436
A : Type ?u.18439
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
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.18436
A : Type ?u.18439
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
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 Hmul
no goals
M : Type u_1
N : Type ?u.18436
A : Type ?u.18439
inst✝¹ : Mul M
s✝ : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
p : M → Prop
x : M
s : Set M
hs : closure s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
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