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

Tactic:
induction x with simp [*]