-- Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
x x_1 x_2 : HopfAlgCat R
h :
  ∀ (x_3 : x.carrier) (x_4 : x_1.carrier) (x_5 : x_2.carrier),
    Eq (α :=
      (Functor.obj
          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
            (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
          (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier)
      ((((((LinearMap.compr₂ₛₗ (TensorProduct.mk R x.carrier x_1.carrier)
                          (LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R)
                            (TensorProduct.mk R (tensorObj (𝒞 := category) x x_1).carrier x_2.carrier)
                            ((fun
                                  (x_6 :
                                    (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1)
                                            x_2)).carrier →ₐc[R]
                                      (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) ↦
                                ((↑x_6 :
                                    [inst_1 :
                                        FunLike
                                          (((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                                      [SemilinearMapClass
                                            (((forget₂ (HopfAlgCat R) (BialgCat R)).obj
                                                  ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                                            (RingHom.id R)
                                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₗ[R]
                                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier) :
                                  (Functor.obj
                                        (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                          fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                          BialgCat.carrier))
                                        (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1) x_2)).carrier →ₗ[R]
                                    (Functor.obj
                                        (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                          fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                          BialgCat.carrier))
                                        (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier))
                              (BialgCat.Hom.toBialgHom'
                                (CategoryTheory.Functor.map
                                  (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                    x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                    fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                                  (Iso.hom (α_ x x_1 x_2)))))) :
                        (a : x.carrier) →
                          x_1.carrier →ₗ[R]
                            x_2.carrier →ₗ[R] ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                      x_3 :
                    x_1.carrier →ₗ[R]
                      x_2.carrier →ₗ[R]
                        (Functor.obj
                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                              (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦
                              x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                            (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) :
                  (a : x_1.carrier) →
                    x_2.carrier →ₗ[R] ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                x_4 :
              x_2.carrier →ₗ[R]
                (Functor.obj
                    (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                      carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                      BialgCat.carrier))
                    (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) :
            (a : x_2.carrier) → ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
          x_5 :
        (Functor.obj
            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
              (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
            (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier)
      ((((((LinearMap.compr₂ₛₗ (TensorProduct.mk R x.carrier x_1.carrier)
                          (LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R)
                            (TensorProduct.mk R (tensorObj (𝒞 := category) x x_1).carrier x_2.carrier)
                            ((fun
                                  (x_6 :
                                    (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1)
                                            x_2)).carrier →ₐc[R]
                                      (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) ↦
                                ((↑x_6 :
                                    [inst_1 :
                                        FunLike
                                          (((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                                      [SemilinearMapClass
                                            (((forget₂ (HopfAlgCat R) (BialgCat R)).obj
                                                  ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                                            (RingHom.id R)
                                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₗ[R]
                                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier) :
                                  (Functor.obj
                                        (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                          fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                          BialgCat.carrier))
                                        (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1) x_2)).carrier →ₗ[R]
                                    (Functor.obj
                                        (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                          x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                          fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                          BialgCat.carrier))
                                        (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier))
                              ((Iso.symm
                                        (Iso.refl
                                          (tensorObj (𝒞 := BialgCat.category)
                                            (Functor.obj
                                              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                BialgCat.carrier))
                                              (tensorObj (𝒞 := category) x x_1))
                                            (Functor.obj
                                              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                BialgCat.carrier))
                                              x_2))) ≪≫
                                      (Iso.symm
                                          (Iso.refl
                                            (tensorObj (𝒞 := BialgCat.category)
                                              (Functor.obj
                                                (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                  x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                  fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                  BialgCat.carrier))
                                                x)
                                              (Functor.obj
                                                (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                  x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                  fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                  BialgCat.carrier))
                                                x_1))) ⊗ᵢ
                                        Iso.refl
                                          (Functor.obj
                                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                              x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                              fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                              BialgCat.carrier))
                                            x_2))) ≪≫
                                    α_
                                        (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          x)
                                        (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          x_1)
                                        (Functor.obj
                                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                            x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                            fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                            BialgCat.carrier))
                                          x_2) ≪≫
                                      (Iso.refl
                                            (Functor.obj
                                              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                BialgCat.carrier))
                                              x) ⊗ᵢ
                                          Iso.refl
                                            (tensorObj (𝒞 := BialgCat.category)
                                              (Functor.obj
                                                (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                  x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                  fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                  BialgCat.carrier))
                                                x_1)
                                              (Functor.obj
                                                (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                  x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                  fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                  BialgCat.carrier))
                                                x_2))) ≪≫
                                        Iso.refl
                                          (tensorObj (𝒞 := BialgCat.category)
                                            (Functor.obj
                                              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                BialgCat.carrier))
                                              x)
                                            (Functor.obj
                                              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦
                                                x1.carrier →ₐc[R] x2.carrier) (CC := carrier) (BialgCat R) (FD :=
                                                fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                                                BialgCat.carrier))
                                              (tensorObj (𝒞 := category) x_1 x_2)))).hom.toBialgHom')) :
                        (a : x.carrier) →
                          x_1.carrier →ₗ[R]
                            x_2.carrier →ₗ[R] ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                      x_3 :
                    x_1.carrier →ₗ[R]
                      x_2.carrier →ₗ[R]
                        (Functor.obj
                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                              (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦
                              x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                            (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) :
                  (a : x_1.carrier) →
                    x_2.carrier →ₗ[R] ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                x_4 :
              x_2.carrier →ₗ[R]
                (Functor.obj
                    (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                      carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                      BialgCat.carrier))
                    (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) :
            (a : x_2.carrier) → ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
          x_5 :
        (Functor.obj
            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
              (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
            (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier)
⊢ Eq (α :=
    x.carrier →ₗ[R]
      x_1.carrier →ₗ[R]
        x_2.carrier →ₗ[R]
          (Functor.obj
              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
                (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
              (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier)
    (LinearMap.compr₂ₛₗ (TensorProduct.mk R x.carrier x_1.carrier)
      (LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R)
        (TensorProduct.mk R (tensorObj (𝒞 := category) x x_1).carrier x_2.carrier)
        ((fun
              (x_3 :
                (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1) x_2)).carrier →ₐc[R]
                  (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) ↦
            ((↑x_3 :
                [inst_1 :
                    FunLike
                      (((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                  [SemilinearMapClass
                        (((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                        (RingHom.id R) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₗ[R]
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier) :
              (Functor.obj
                    (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                      carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                      BialgCat.carrier))
                    (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1) x_2)).carrier →ₗ[R]
                (Functor.obj
                    (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                      carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                      BialgCat.carrier))
                    (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier))
          (BialgCat.Hom.toBialgHom'
            (CategoryTheory.Functor.map
              (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier)
                (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
              (Iso.hom (α_ x x_1 x_2)))))))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk R x.carrier x_1.carrier)
      (LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R)
        (TensorProduct.mk R (tensorObj (𝒞 := category) x x_1).carrier x_2.carrier)
        ((fun
              (x_3 :
                (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1) x_2)).carrier →ₐc[R]
                  (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier) ↦
            ((↑x_3 :
                [inst_1 :
                    FunLike
                      (((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                  [SemilinearMapClass
                        (((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₐc[R]
                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier)
                        (RingHom.id R) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier] →
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj ((x ⊗ x_1) ⊗ x_2)).carrier →ₗ[R]
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x ⊗ x_1 ⊗ x_2)).carrier) :
              (Functor.obj
                    (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                      carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                      BialgCat.carrier))
                    (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) x x_1) x_2)).carrier →ₗ[R]
                (Functor.obj
                    (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                      carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                      BialgCat.carrier))
                    (tensorObj (𝒞 := category) x (tensorObj (𝒞 := category) x_1 x_2))).carrier))
          ((Iso.symm
                    (Iso.refl
                      (tensorObj (𝒞 := BialgCat.category)
                        (Functor.obj
                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CD := BialgCat.carrier))
                          (tensorObj (𝒞 := category) x x_1))
                        (Functor.obj
                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CD := BialgCat.carrier))
                          x_2))) ≪≫
                  (Iso.symm
                      (Iso.refl
                        (tensorObj (𝒞 := BialgCat.category)
                          (Functor.obj
                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                              (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦
                              x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                            x)
                          (Functor.obj
                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                              (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦
                              x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                            x_1))) ⊗ᵢ
                    Iso.refl
                      (Functor.obj
                        (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                          carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                          BialgCat.carrier))
                        x_2))) ≪≫
                α_
                    (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      x)
                    (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      x_1)
                    (Functor.obj
                      (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
                        carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
                        BialgCat.carrier))
                      x_2) ≪≫
                  (Iso.refl
                        (Functor.obj
                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CD := BialgCat.carrier))
                          x) ⊗ᵢ
                      Iso.refl
                        (tensorObj (𝒞 := BialgCat.category)
                          (Functor.obj
                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                              (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦
                              x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                            x_1)
                          (Functor.obj
                            (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                              (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦
                              x1.carrier →ₐc[R] x2.carrier) (CD := BialgCat.carrier))
                            x_2))) ≪≫
                    Iso.refl
                      (tensorObj (𝒞 := BialgCat.category)
                        (Functor.obj
                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CD := BialgCat.carrier))
                          x)
                        (Functor.obj
                          (forget₂ (HopfAlgCat R) (FC := fun (x1 x2 : HopfAlgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CC := carrier) (BialgCat R) (FD := fun (x1 x2 : BialgCat R) ↦ x1.carrier →ₐc[R] x2.carrier)
                            (CD := BialgCat.carrier))
                          (tensorObj (𝒞 := category) x_1 x_2)))).hom.toBialgHom')))

Tactic:
ext