Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: 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✝

Tactic:
;

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✝