-- Lean 4 proof step from Mathlib.Algebra.Category.BialgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
x : BialgCat R
⊢ AlgHom.comp
      (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.includeLeft =
    (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))
                        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))
                        ((𝟙_ (BialgCat R)) (𝒞 := category))))) ≪≫
                (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) ⊗ᵢ
                  Iso.symm (Iso.refl ((𝟙_ (AlgCat R)) (𝒞 := 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)).hom).comp
      Algebra.TensorProduct.includeLeft
have 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
            (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.includeLeft :
          (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))
    (((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))
                              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))
                              ((𝟙_ (BialgCat R)) (𝒞 := category))))) ≪≫
                      (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) ⊗ᵢ
                        Iso.symm (Iso.refl ((𝟙_ (AlgCat R)) (𝒞 := 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)).hom).comp
            Algebra.TensorProduct.includeLeft :
          (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))
Tactic: ext