-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
x : FreeMonoid α
one :
  Eq.{u_1 + 1} (α := FreeMonoid α)
    ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
              toFreeMonoid :
            WithOne (FreeSemigroup α) →* FreeMonoid α) :
          (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
        (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
              (a : FreeMonoid α) → WithOne (FreeSemigroup α))
            1 :
          WithOne (FreeSemigroup α)) :
      FreeMonoid α)
    (1 : FreeMonoid α)
of :
  ∀ (x : α),
    (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
            WithOne (FreeSemigroup α) →* FreeMonoid α) :
          (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
        (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
              (a : FreeMonoid α) → WithOne (FreeSemigroup α))
            (FreeMonoid.of x) :
          WithOne (FreeSemigroup α)) =
      FreeMonoid.of x
⊢ (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
          WithOne (FreeSemigroup α) →* FreeMonoid α) :
        (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
      (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          x :
        WithOne (FreeSemigroup α)) =
    x
have mul : ∀ (x y : FreeMonoid α),
  (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
            WithOne (FreeSemigroup α) →* FreeMonoid α) :
          (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
        (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
              (a : FreeMonoid α) → WithOne (FreeSemigroup α))
            x :
          WithOne (FreeSemigroup α)) =
      x →
    (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α) toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                  (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
                (a : FreeMonoid α) → WithOne (FreeSemigroup α))
              y :
            WithOne (FreeSemigroup α)) =
        y →
      (((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
                  (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
                (a : FreeMonoid α) → WithOne (FreeSemigroup α))
              (x * y) :
            WithOne (FreeSemigroup α)) =
        x * y
Tactic: induction x with simp [*]
Cleared hypotheses: x