-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
s : Set M
motive : (m : M) → Membership.mem (γ := Submonoid M) (closure s) m → Prop
one : motive 1 ⋯
mul_left :
  ∀ (x : M) (hx : x ∈ s) (y : M) (hy : Membership.mem (γ := Submonoid M) (closure s) y), motive y hy → motive (x * y) ⋯
l : FreeMonoid { x : M // x ∈ s }
h :
  Membership.mem (α := M) (γ := Submonoid M) (closure s)
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        l :
      M)
one₁ :
  ∀
    (h :
      Membership.mem (α := M) (γ := Submonoid M) (closure s)
        ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                  (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
                FreeMonoid { x : M // x ∈ s } →* M) :
              (a : FreeMonoid { x : M // x ∈ s }) → M)
            1 :
          M)),
    motive
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
              (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
            FreeMonoid { x : M // x ∈ s } →* M) :
          (a : FreeMonoid { x : M // x ∈ s }) → M)
        1)
      h
⊢ motive
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      l)
    h
have mul_of : ∀ (x : { x : M // x ∈ s }) (y : FreeMonoid { x : M // x ∈ s })
  (ih :
    ∀
      (h :
        Membership.mem (α := M) (γ := Submonoid M) (closure s)
          ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                    (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
                  FreeMonoid { x : M // x ∈ s } →* M) :
                (a : FreeMonoid { x : M // x ∈ s }) → M)
              y :
            M)),
      motive
        ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
              FreeMonoid { x : M // x ∈ s } →* M) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          y)
        h)
  (h :
    Membership.mem (α := M) (γ := Submonoid M) (closure s)
      ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
                (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
              FreeMonoid { x : M // x ∈ s } →* M) :
            (a : FreeMonoid { x : M // x ∈ s }) → M)
          (FreeMonoid.of x * y) :
        M)),
  motive
    ((((FreeMonoid.lift : (a : { x : M // x ∈ s } → M) → FreeMonoid { x : M // x ∈ s } →* M)
            (Subtype.val (p := fun (x : M) ↦ x ∈ s)) :
          FreeMonoid { x : M // x ∈ s } →* M) :
        (a : FreeMonoid { x : M // x ∈ s }) → M)
      (FreeMonoid.of x * y))
    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]
Cleared hypotheses: l, h