-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem closure_induction_left {s : Set M} {p : (m : M) → m ∈ closure s → Prop}
    (one : p 1 (one_mem _))
    (mul_left : ∀ x (hx : x ∈ s), ∀ (y) hy, p y hy → p (x * y) (mul_mem (subset_closure hx) hy))
    {x : M} (h : x ∈ closure s) :
    p x h

Proof state:
case intro.mul_of
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), p ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ (FreeMonoid.lift Subtype.val) y ∈ closure s

Tactic:
simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Result:
no goals

Proof state:
case intro.one
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
h : (FreeMonoid.lift Subtype.val) 1 ∈ closure s
⊢ p ((FreeMonoid.lift Subtype.val) 1) h

Tactic:
exact one

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
l : FreeMonoid { x // x ∈ s }
h : (FreeMonoid.lift Subtype.val) l ∈ closure s
⊢ p ((FreeMonoid.lift Subtype.val) l) h

Tactic:
induction l using FreeMonoid.inductionOn' with
| one => exact one
| mul_of x y ih =>
  simp only [map_mul, FreeMonoid.lift_eval_of]
  refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)
  simp only [closure_eq_mrange, mem_mrange, exists_apply_eq_apply]

Result:
no goals

Proof state:
case intro.mul_of
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), p ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ p (↑x * (FreeMonoid.lift Subtype.val) y) ⋯

Tactic:
refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)

Result:
case intro.mul_of
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), p ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ (FreeMonoid.lift Subtype.val) y ∈ closure s

Proof state:
case intro.mul_of
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), p ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ p ((FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y)) h

Tactic:
simp only [map_mul, FreeMonoid.lift_eval_of]

Result:
case intro.mul_of
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), p ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ p (↑x * (FreeMonoid.lift Subtype.val) y) ⋯

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : M
h✝ : x ∈ closure s
h : x ∈ mrange (FreeMonoid.lift Subtype.val)
⊢ p x h✝

Tactic:
obtain ⟨l, rfl⟩ := h

Result:
case intro
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
l : FreeMonoid { x // x ∈ s }
h : (FreeMonoid.lift Subtype.val) l ∈ closure s
⊢ p ((FreeMonoid.lift Subtype.val) l) h

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : M
h : x ∈ closure s
⊢ p x h

Tactic:
simp_rw [closure_eq_mrange] at h

Result:
M : Type u_1
inst✝ : Monoid M
s : Set M
p : (m : M) → m ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
x : M
h✝ : x ∈ closure s
h : x ∈ mrange (FreeMonoid.lift Subtype.val)
⊢ p x h✝