-- Lean 4 proof step from Mathlib.Algebra.Category.HopfAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
X₁ Y₁ X₂ Y₂ : HopfAlgCat R
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
⊢ 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))
      (x ⊗ₘ x_1) =
    Iso.inv
        (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₂))) ≫
      (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))
            x ⊗ₘ
          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))
            x_1) ≫
        Iso.hom
          (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))
                Y₁)
              (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))
                Y₂)))
have h : ∀
  (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₁ 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))
        (tensorObj (𝒞 := category) Y₁ Y₂)).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))
              (x ⊗ₘ x_1)) :
          (a : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁ ⊗ X₂)).carrier) →
            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (Y₁ ⊗ Y₂)).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))
          (tensorObj (𝒞 := category) Y₁ Y₂)).carrier)
    ((BialgCat.Hom.toBialgHom
            (Iso.inv
                (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₂))) ≫
              (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))
                    x ⊗ₘ
                  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))
                    x_1) ≫
                Iso.hom
                  (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))
                        Y₁)
                      (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))
                        Y₂)))) :
          (a : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁ ⊗ X₂)).carrier) →
            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (Y₁ ⊗ Y₂)).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))
          (tensorObj (𝒞 := category) Y₁ Y₂)).carrier)
Tactic: ext