M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
x : M
h : x ∈ mrange (↑FreeMonoid.lift Subtype.val)
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p x
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
x : M
h : x ∈ closure s
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p x
rw [closure_eq_mrange] at h
case intro
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
l : FreeMonoid { x // x ∈ s }
⊢ p (↑(↑FreeMonoid.lift Subtype.val) l)
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
x : M
h : x ∈ mrange (↑FreeMonoid.lift Subtype.val)
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p x
obtain ⟨l, rfl⟩ := h
case intro.h0
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p (↑(↑FreeMonoid.lift Subtype.val) 1)

case intro.ih
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : p (↑(↑FreeMonoid.lift Subtype.val) y)
⊢ p (↑(↑FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y))
case intro
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
l : FreeMonoid { x // x ∈ s }
⊢ p (↑(↑FreeMonoid.lift Subtype.val) l)
induction' l using FreeMonoid.recOn with x y ih
no goals
case intro.h0
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
⊢ p (↑(↑FreeMonoid.lift Subtype.val) 1)
exact H1
no goals
case intro.ih
M : Type u_1
A : Type ?u.83795
B : Type ?u.83798
inst✝ : Monoid M
s : Set M
p : M → Prop
H1 : p 1
Hmul : ∀ (x : M), x ∈ s → ∀ (y : M), p y → p (x * y)
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : p (↑(↑FreeMonoid.lift Subtype.val) y)
⊢ p (↑(↑FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y))
simpa only [map_mul, FreeMonoid.lift_eval_of] using Hmul _ x.prop _ ih