Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : HopfAlgCat R
⊢ (TensorProduct.mk R x✝².carrier x✝¹.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (x✝² ⊗ x✝¹).carrier x✝.carrier).compr₂ₛₗ
        ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (α_ x✝² x✝¹ x✝).hom).toBialgHom')) =
    (TensorProduct.mk R x✝².carrier x✝¹.carrier).compr₂ₛₗ
      ((TensorProduct.mk R (x✝² ⊗ x✝¹).carrier x✝.carrier).compr₂ₛₗ
        ((fun x ↦ ↑x)
          (((Iso.refl
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝² ⊗ x✝¹) ⊗
                        (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).symm ≪≫
                  ((Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝² ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).symm ⊗ᵢ
                    Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝))) ≪≫
                α_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)
                    ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝) ≪≫
                  (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²) ⊗ᵢ
                      Iso.refl
                        ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹ ⊗
                          (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)) ≪≫
                    Iso.refl
                      ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝² ⊗
                        (forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝¹ ⊗ x✝))).hom.toBialgHom'))

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝⁵ x✝⁴ x✝³ : HopfAlgCat R
x✝² : x✝⁵.carrier
x✝¹ : x✝⁴.carrier
x✝ : x✝³.carrier
⊢ ((((TensorProduct.mk R x✝⁵.carrier x✝⁴.carrier).compr₂ₛₗ
            ((TensorProduct.mk R (x✝⁵ ⊗ x✝⁴).carrier x✝³.carrier).compr₂ₛₗ
              ((fun x ↦ ↑x) ((forget₂ (HopfAlgCat R) (BialgCat R)).map (α_ x✝⁵ x✝⁴ x✝³).hom).toBialgHom')))
          x✝²)
        x✝¹)
      x✝ =
    ((((TensorProduct.mk R x✝⁵.carrier x✝⁴.carrier).compr₂ₛₗ
            ((TensorProduct.mk R (x✝⁵ ⊗ x✝⁴).carrier x✝³.carrier).compr₂ₛₗ
              ((fun x ↦ ↑x)
                (((Iso.refl
                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁵ ⊗ x✝⁴) ⊗
                              (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)).symm ≪≫
                        ((Iso.refl
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵ ⊗
                                (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴)).symm ⊗ᵢ
                          Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³))) ≪≫
                      α_ ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵) ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴)
                          ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³) ≪≫
                        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵) ⊗ᵢ
                            Iso.refl
                              ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁴ ⊗
                                (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³)) ≪≫
                          Iso.refl
                            ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝⁵ ⊗
                              (forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁴ ⊗ x✝³))).hom.toBialgHom')))
          x✝²)
        x✝¹)
      x✝