-- Module: Mathlib.Algebra.Group.Submonoid.Membership
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
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
⊢ 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

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]

Premises used: FreeMonoid.lift_eval_of, map_mul, Submonoid.closure_eq_mrange, MonoidHom.mem_mrange, exists_apply_eq_apply