Module: Mathlib.Algebra.Category.BialgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝².carrier
⊢ ((AlgHom.restrictScalars R
            ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom)).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgCat.Hom.hom
                  (((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                        ((Iso.refl
                              ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                                (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                          Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                      α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                        (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                            Iso.refl
                              ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                                (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : BialgCat R
x✝ : x✝².carrier
⊢ ((AlgHom.restrictScalars R
            ((AlgCat.Hom.hom ((forget₂ (BialgCat R) (AlgCat R)).map (α_ x✝³ x✝² x✝¹).hom)).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgCat.Hom.hom
                  (((Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj (x✝³ ⊗ x✝²) ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)).symm ≪≫
                        ((Iso.refl
                              ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                                (forget₂ (BialgCat R) (AlgCat R)).obj x✝²)).symm ⊗ᵢ
                          Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))) ≪≫
                      α_ ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ((forget₂ (BialgCat R) (AlgCat R)).obj x✝²)
                          ((forget₂ (BialgCat R) (AlgCat R)).obj x✝¹) ≪≫
                        (Iso.refl ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³) ⊗ᵢ
                            Iso.refl
                              ((forget₂ (BialgCat R) (AlgCat R)).obj x✝² ⊗
                                (forget₂ (BialgCat R) (AlgCat R)).obj x✝¹)) ≪≫
                          Iso.refl
                            ((forget₂ (BialgCat R) (AlgCat R)).obj x✝³ ⊗
                              (forget₂ (BialgCat R) (AlgCat R)).obj (x✝² ⊗ x✝¹))).hom).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝