-- Module: Mathlib.Algebra.Category.BialgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : BialgCat R
x_3 : x.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.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.includeLeft :
          (a : x.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))
    (((((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).comp
              Algebra.TensorProduct.includeLeft :
            x.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.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))

Tactic:
rfl