-- Lean 4 proof step from Mathlib.Algebra.Category.BialgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
X₁ X₂ : BialgCat R
x : X₁ ⟶ X₂
x_1 : BialgCat R
⊢ 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_1))) ≫
      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 ▷
          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_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))
                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_1)))
have 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_1)) :
      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) X₂ x_1)) :
      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_1)) : Type u)) →
            (↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₂ ⊗ x_1)) : 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) X₂ x_1)) :
        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_1))) ≫
              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 ▷
                  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_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))
                        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_1)))) :
          (a : (↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₁ ⊗ x_1)) : Type u)) →
            (↑((forget₂ (BialgCat R) (AlgCat R)).obj (X₂ ⊗ x_1)) : 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) X₂ x_1)) :
        Type u))
Tactic: ext