-- Module: Mathlib.Algebra.Category.BialgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
x : BialgCat R
H :
  ∀ (x_1 : 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))
            x) :
        Type u))
      ((AlgHom.comp
              (AlgHom.restrictScalars R (S := R)
                (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)))))
              Algebra.TensorProduct.includeRight :
            (a : x.carrier) → (↑((forget₂ (BialgCat R) (AlgCat R)).obj x) : Type u))
          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) :
          Type u))
      ((AlgHom.comp
              (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))
                                ((𝟙_ (BialgCat R)) (𝒞 := category)))
                              (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.symm (Iso.refl ((𝟙_ (AlgCat R)) (𝒞 := AlgCat.instCategory R))) ⊗ᵢ
                          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))) ≪≫
                      λ_
                        (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)).hom))
              Algebra.TensorProduct.includeRight :
            (a : x.carrier) → (↑((forget₂ (BialgCat R) (AlgCat R)).obj x) : Type u))
          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) :
          Type u))
⊢ Eq (α :=
    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))
            x) :
        Type u))
    (AlgHom.comp
      (AlgHom.restrictScalars R (S := R)
        (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)))))
      Algebra.TensorProduct.includeRight)
    (AlgHom.comp
      (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))
                        ((𝟙_ (BialgCat R)) (𝒞 := category)))
                      (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.symm (Iso.refl ((𝟙_ (AlgCat R)) (𝒞 := AlgCat.instCategory R))) ⊗ᵢ
                  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))) ≪≫
              λ_
                (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)).hom))
      Algebra.TensorProduct.includeRight)

Tactic:
ext