-- Module: Mathlib.Algebra.Category.BialgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
X₁ Y₁ X₂ Y₂ : BialgCat R
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
hf :
  ∀
    (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))
            (tensorObj (𝒞 := category) X₁ X₂)) :
        Type u)),
    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) Y₁ Y₂)) :
        Type u))
      ((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))
                (x ⊗ₘ x_1)) :
            (a : (↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁ ⊗ X₂)) : Type u)) →
              (↑((forget₂ (BialgCat R) (AlgCat R)).obj (Y₁ ⊗ Y₂)) : Type u))
          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))
              (tensorObj (𝒞 := category) Y₁ Y₂)) :
          Type u))
      ((AlgCat.Hom.hom
              (Iso.inv
                  (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₂))) ≫
                (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))
                      x ⊗ₘ
                    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))
                      x_1) ≫
                  Iso.hom
                    (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))
                          Y₁)
                        (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))
                          Y₂)))) :
            (a : (↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁ ⊗ X₂)) : Type u)) →
              (↑((forget₂ (BialgCat R) (AlgCat R)).obj (Y₁ ⊗ Y₂)) : Type u))
          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))
              (tensorObj (𝒞 := category) Y₁ Y₂)) :
          Type u))
⊢ 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))
      (x ⊗ₘ x_1) =
    Iso.inv
        (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₂))) ≫
      (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))
            x ⊗ₘ
          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))
            x_1) ≫
        Iso.hom
          (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))
                Y₁)
              (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))
                Y₂)))

Tactic:
ext