-- Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
x : HopfAlgCat R
x_1 : x.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))
        x).carrier)
    (((LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R)
                (TensorProduct.mk R (carrier (R := R) ((𝟙_ (HopfAlgCat R)) (𝒞 := category))) x.carrier)
                ((fun
                      (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))
                              (tensorObj (𝒞 := category) ((𝟙_ (HopfAlgCat R)) (𝒞 := category)) x)).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))
                              x).carrier) ↦
                    ((↑x_2 :
                        [inst_1 :
                            FunLike
                              (((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier →ₐc[R]
                                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier)
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier] →
                          [SemilinearMapClass
                                (((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier →ₐc[R]
                                  ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier)
                                (RingHom.id R)
                                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier
                                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier] →
                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier →ₗ[R]
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).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) ((𝟙_ (HopfAlgCat R)) (𝒞 := category)) x)).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))
                            x).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))))) :
              (a : R) → x.carrier →ₗ[R] ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier)
            1 :
          (a : x.carrier) → ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).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).carrier)
    (((LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R)
                (TensorProduct.mk R (carrier (R := R) ((𝟙_ (HopfAlgCat R)) (𝒞 := category))) x.carrier)
                ((fun
                      (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))
                              (tensorObj (𝒞 := category) ((𝟙_ (HopfAlgCat R)) (𝒞 := category)) x)).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))
                              x).carrier) ↦
                    ((↑x_2 :
                        [inst_1 :
                            FunLike
                              (((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier →ₐc[R]
                                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier)
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier] →
                          [SemilinearMapClass
                                (((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier →ₐc[R]
                                  ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier)
                                (RingHom.id R)
                                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier
                                ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier] →
                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (𝟙_ (HopfAlgCat R) ⊗ x)).carrier →ₗ[R]
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).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) ((𝟙_ (HopfAlgCat R)) (𝒞 := category)) x)).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))
                            x).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))
                                  ((𝟙_ (HopfAlgCat R)) (𝒞 := 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))) ≪≫
                          (Iso.symm (Iso.refl ((𝟙_ (BialgCat R)) (𝒞 := BialgCat.category))) ⊗ᵢ
                            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))) ≪≫
                        λ_
                          (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)).hom.toBialgHom') :
              (a : R) → x.carrier →ₗ[R] ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).carrier)
            1 :
          (a : x.carrier) → ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x).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).carrier)

Tactic:
rfl