-- Module: Mathlib.LinearAlgebra.FreeProduct.Basic
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
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))
                              ⋯) :
                          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)
⊢ (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

Tactic:
ext i a