-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeProduct.Basic (goal)
Goal:
I : Type u
inst : DecidableEq I
i : I
R : Type v
inst_1 : CommSemiring R
A : I → Type w
inst_2 : (i : I) → Semiring (A i)
inst_3 : (i : I) → Algebra.{v, w} R (A i)
B : Type w'
inst_4 : Semiring B
inst_5 : Algebra R B
maps_1 : {i : I} → AlgHom.{v, w, w'} R (A i) B
maps : FreeProduct R A →ₐ[R] B
⊢ (fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
        ((liftAlgHom R (s := rel R A) :
              (a :
                  { f : FreeTensorAlgebra R A →ₐ[R] B //
                    ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                      rel R A x y →
                        (f : (a : FreeTensorAlgebra R A) → B) x = (f : (a : FreeTensorAlgebra R A) → B) y }) →
                RingQuot (rel R A) →ₐ[R] B)
            (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
              ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                rel R A x y →
                  Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                    ((f : (a : FreeTensorAlgebra R A) → B) y : B))
              ((TensorAlgebra.lift R : (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
              ⋯) :
          RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
      ((fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i) maps) =
    maps
have w : ∀ (i : I) (a : A i),
  Eq.{w' + 1} (α := B)
    (((AlgHom.toLinearMap
                (AlgHom.comp (B := RingQuot (R := FreeTensorAlgebra R A) (rel R A))
                  ((fun (maps : {i : I} → AlgHom.{v, w, w'} R (A i) B) ↦
                      ((liftAlgHom R (s := rel R A) :
                            (a :
                                { f : FreeTensorAlgebra R A →ₐ[R] B //
                                  ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                                    rel R A x y →
                                      (f : (a : FreeTensorAlgebra R A) → B) x =
                                        (f : (a : FreeTensorAlgebra R A) → B) y }) →
                              RingQuot (rel R A) →ₐ[R] B)
                          (Subtype.mk (p := fun (f : FreeTensorAlgebra R A →ₐ[R] B) ↦
                            ∀ ⦃x y : FreeTensorAlgebra R A⦄,
                              rel R A x y →
                                Eq.{w' + 1} (α := B) ((f : (a : FreeTensorAlgebra R A) → B) x : B)
                                  ((f : (a : FreeTensorAlgebra R A) → B) y : B))
                            ((TensorAlgebra.lift R :
                                (a : (⨁ (i : I), A i) →ₗ[R] B) → TensorAlgebra R (⨁ (i : I), A i) →ₐ[R] B)
                              (toModule R I (M := A) B fun (x : I) ↦ AlgHom.toLinearMap maps))
                            sorry) :
                        RingQuot (R := FreeTensorAlgebra R A) (rel R A) →ₐ[R] B))
                    ((fun (π : FreeProduct R A →ₐ[R] B) (i : I) ↦ π ∘ₐ ι R A i) maps))
                  (RingQuot.mkAlgHom R (rel R A))) ∘ₗ
              TensorAlgebra.ι R) ∘ₗ
            DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)
    ((((maps ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i :
          (a : A i) → B)
        a :
      B)
Tactic: ext i a