-- Module: Mathlib.Algebra.Category.BialgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : BialgCat R
H :
  ∀ (x_3 : x_1.carrier),
    Eq (α :=
      (↑(Functor.obj
            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
              (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
            (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))) :
        Type u))
      ((AlgHom.comp (B := x.carrier ⊗[R] x_1.carrier)
              (AlgHom.restrictScalars R
                (AlgHom.comp
                  (AlgCat.Hom.hom
                    (CategoryTheory.Functor.map
                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                        AlgCat.carrier))
                      (Iso.hom (α_ x x_1 x_2))))
                  Algebra.TensorProduct.includeLeft))
              Algebra.TensorProduct.includeRight :
            (a : x_1.carrier) → (↑((forget₂ (BialgCat R) (AlgCat R)).obj (x ⊗ x_1 ⊗ x_2)) : Type u))
          x_3 :
        (↑(Functor.obj
              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
                (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
              (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))) :
          Type u))
      (((AlgHom.comp (B := x.carrier ⊗[R] x_1.carrier)
                (AlgHom.restrictScalars R
                  ((AlgCat.Hom.hom
                        ((Iso.symm
                                (Iso.refl
                                  (tensorObj (𝒞 := AlgCat.instCategory R)
                                    (Functor.obj
                                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                        x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                        fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                        AlgCat.carrier))
                                      (tensorObj (𝒞 := category) x x_1))
                                    (Functor.obj
                                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                        x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                        fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                        AlgCat.carrier))
                                      x_2))) ≪≫
                              (Iso.symm
                                  (Iso.refl
                                    (tensorObj (𝒞 := AlgCat.instCategory R)
                                      (Functor.obj
                                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                          fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                          AlgCat.carrier))
                                        x)
                                      (Functor.obj
                                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                          fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                          AlgCat.carrier))
                                        x_1))) ⊗ᵢ
                                Iso.refl
                                  (Functor.obj
                                    (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                      x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                      fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                      AlgCat.carrier))
                                    x_2))) ≪≫
                            α_
                                (Functor.obj
                                  (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                    (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                    (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                                  x)
                                (Functor.obj
                                  (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                    (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                    (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                                  x_1)
                                (Functor.obj
                                  (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                    (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                    (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                                  x_2) ≪≫
                              (Iso.refl
                                    (Functor.obj
                                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                        x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                        fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                        AlgCat.carrier))
                                      x) ⊗ᵢ
                                  Iso.refl
                                    (tensorObj (𝒞 := AlgCat.instCategory R)
                                      (Functor.obj
                                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                          fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                          AlgCat.carrier))
                                        x_1)
                                      (Functor.obj
                                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                          fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                          AlgCat.carrier))
                                        x_2))) ≪≫
                                Iso.refl
                                  (tensorObj (𝒞 := AlgCat.instCategory R)
                                    (Functor.obj
                                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                        x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                        fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                        AlgCat.carrier))
                                      x)
                                    (Functor.obj
                                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦
                                        x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (AlgCat R) (FD :=
                                        fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                                        AlgCat.carrier))
                                      (tensorObj (𝒞 := category) x_1 x_2)))).hom).comp
                    Algebra.TensorProduct.includeLeft))
                Algebra.TensorProduct.includeRight :
              x_1.carrier →ₐ[R]
                (↑(Functor.obj
                      (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD :=
                        AlgCat.carrier))
                      (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))) :
                  Type u)) :
            (a : x_1.carrier) → (↑((forget₂ (BialgCat R) (AlgCat R)).obj (x ⊗ x_1 ⊗ x_2)) : Type u))
          x_3 :
        (↑(Functor.obj
              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
                (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
              (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))) :
          Type u))
⊢ Eq (α :=
    x_1.carrier →ₐ[R]
      (↑(Functor.obj
            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
              (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
            (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))) :
        Type u))
    (AlgHom.comp (B := x.carrier ⊗[R] x_1.carrier)
      (AlgHom.restrictScalars R
        (AlgHom.comp
          (AlgCat.Hom.hom
            (CategoryTheory.Functor.map
              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
                (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
              (Iso.hom (α_ x x_1 x_2))))
          Algebra.TensorProduct.includeLeft))
      Algebra.TensorProduct.includeRight)
    (AlgHom.comp (B := x.carrier ⊗[R] x_1.carrier)
      (AlgHom.restrictScalars R
        ((AlgCat.Hom.hom
              ((Iso.symm
                      (Iso.refl
                        (tensorObj (𝒞 := AlgCat.instCategory R)
                          (Functor.obj
                            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                              carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                              (CD := AlgCat.carrier))
                            (tensorObj (𝒞 := category) x x_1))
                          (Functor.obj
                            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                              carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                              (CD := AlgCat.carrier))
                            x_2))) ≪≫
                    (Iso.symm
                        (Iso.refl
                          (tensorObj (𝒞 := AlgCat.instCategory R)
                            (Functor.obj
                              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                              x)
                            (Functor.obj
                              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                              x_1))) ⊗ᵢ
                      Iso.refl
                        (Functor.obj
                          (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                            carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                            (CD := AlgCat.carrier))
                          x_2))) ≪≫
                  α_
                      (Functor.obj
                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                          carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                          (CD := AlgCat.carrier))
                        x)
                      (Functor.obj
                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                          carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                          (CD := AlgCat.carrier))
                        x_1)
                      (Functor.obj
                        (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                          carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                          (CD := AlgCat.carrier))
                        x_2) ≪≫
                    (Iso.refl
                          (Functor.obj
                            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                              carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                              (CD := AlgCat.carrier))
                            x) ⊗ᵢ
                        Iso.refl
                          (tensorObj (𝒞 := AlgCat.instCategory R)
                            (Functor.obj
                              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                              x_1)
                            (Functor.obj
                              (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                                (CC := carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦
                                (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CD := AlgCat.carrier))
                              x_2))) ≪≫
                      Iso.refl
                        (tensorObj (𝒞 := AlgCat.instCategory R)
                          (Functor.obj
                            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                              carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                              (CD := AlgCat.carrier))
                            x)
                          (Functor.obj
                            (forget₂ (BialgCat R) (FC := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                              carrier) (AlgCat R) (FD := fun (x1 x2 : AlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u))
                              (CD := AlgCat.carrier))
                            (tensorObj (𝒞 := category) x_1 x_2)))).hom).comp
          Algebra.TensorProduct.includeLeft))
      Algebra.TensorProduct.includeRight)

Tactic:
ext