-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
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 α))
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 α))
⊢ ((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 α))

Tactic:
induction a with simp_all