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

Tactic:
ext