-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (Function.comp (β := FreeAlgebra R M)
      (⇑(AlgHom.comp (B := RingQuot (R := FreeAlgebra R M) (Rel R M))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              ((fun (F : TensorAlgebra R M →ₐ[R] A) ↦ F.toLinearMap ∘ₗ ι R) F))
            (RingQuot.mkAlgHom R (Rel R M))) :
        (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R M) (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) : (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
have rw : Eq.{u_3 + 1} (α := A)
  (Function.comp (β := FreeAlgebra R M)
    (⇑(AlgHom.comp (B := RingQuot (R := FreeAlgebra R M) (Rel R M))
          (Function.comp (β :=
            { f : FreeAlgebra R M →ₐ[R] A //
              ∀ ⦃x y : FreeAlgebra R M⦄,
                Rel R M x y →
                  Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                    ((f : (a : FreeAlgebra R M) → A) y : A) })
            (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
              (a :
                  { f : FreeAlgebra R M →ₐ[R] A //
                    ∀ ⦃x y : FreeAlgebra R M⦄,
                      Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                RingQuot (Rel R M) →ₐ[R] A)
            (fun (f : M →ₗ[R] A) ↦
              Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A))
                ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) sorry)
            ((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
                (F.toLinearMap ∘ₗ
                    {
                      toFun := fun (m : M) ↦
                        (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
                          (FreeAlgebra.ι R m),
                      map_add' := sorry, map_smul' := sorry } :
                  M →ₗ[R] A))
              F))
          (RingQuot.mkAlgHom R (Rel R M))) :
      (a : FreeAlgebra R M) → A)
    (FreeAlgebra.ι R) x)
  (Function.comp (β := FreeAlgebra R M) (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) : (a : FreeAlgebra R M) → A)
    (FreeAlgebra.ι R) x)
Tactic: rw [ι]