-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.FreeSemigroup (goal)
Goal:
α : Type u_1
a : FreeSemigroup α
coe :
  ∀ (x : α),
    ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          (a : FreeMonoid α) → WithOne (FreeSemigroup α))
        ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                  toFreeMonoid :
                WithOne (FreeSemigroup α) →* FreeMonoid α) :
              (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          FreeMonoid α) =
      (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α))
⊢ ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
          (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
        (a : FreeMonoid α) → WithOne (FreeSemigroup α))
      ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                toFreeMonoid :
              WithOne (FreeSemigroup α) →* FreeMonoid α) :
            (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
          (↑a : WithOne (FreeSemigroup α)) :
        FreeMonoid α) =
    (↑a : WithOne (FreeSemigroup α))
have coe₁ : ∀ (x : α) (y : FreeSemigroup α),
  ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          (a : FreeMonoid α) → WithOne (FreeSemigroup α))
        ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                  toFreeMonoid :
                WithOne (FreeSemigroup α) →* FreeMonoid α) :
              (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
            (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
          FreeMonoid α) =
      (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) →
    ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                    toFreeMonoid :
                  WithOne (FreeSemigroup α) →* FreeMonoid α) :
                (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
              (↑y : WithOne (FreeSemigroup α)) :
            FreeMonoid α) =
        (↑y : WithOne (FreeSemigroup α)) →
      ((lift : (a : α → WithOne (FreeSemigroup α)) → FreeMonoid α →* WithOne (FreeSemigroup α)) fun (x : α) ↦
              (↑(FreeSemigroup.of x) : WithOne (FreeSemigroup α)) :
            (a : FreeMonoid α) → WithOne (FreeSemigroup α))
          ((((WithOne.lift : (a : FreeSemigroup α →ₙ* FreeMonoid α) → WithOne (FreeSemigroup α) →* FreeMonoid α)
                    toFreeMonoid :
                  WithOne (FreeSemigroup α) →* FreeMonoid α) :
                (a : WithOne (FreeSemigroup α)) → FreeMonoid α)
              (↑(FreeSemigroup.of x * y) : WithOne (FreeSemigroup α)) :
            FreeMonoid α) =
        (↑(FreeSemigroup.of x * y) : WithOne (FreeSemigroup α))
Tactic: induction a with simp_all
Cleared hypotheses: a