Module: Mathlib.Algebra.Homology.LeftResolution.Transport

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A'
eA : A' ≌ A
eC : C' ≌ C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x✝ : A'
⊢ Epi
    ((((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').rightUnitor.inv ≫
          ((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').whiskerLeft eA.unitIso.hom ≫
            ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator ι' (eA.functor ⋙ eA.inverse)).hom ≫
              (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (ι'.associator eA.functor eA.inverse).inv ≫
                (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (whiskerRight e.hom eA.inverse) ≫
                  ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator (eC.functor ⋙ ι) eA.inverse).inv ≫
                    whiskerRight ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator eC.functor ι).inv eA.inverse ≫
                      whiskerRight (whiskerRight (eA.functor.associator (Λ.F ⋙ eC.inverse) eC.functor).hom ι)
                          eA.inverse ≫
                        whiskerRight
                            (whiskerRight
                              (eA.functor.whiskerLeft
                                ((Λ.F.associator eC.inverse eC.functor).hom ≫
                                  Λ.F.whiskerLeft eC.counitIso.hom ≫ Λ.F.rightUnitor.hom))
                              ι)
                            eA.inverse ≫
                          whiskerRight
                              ((eA.functor.associator Λ.F ι).hom ≫
                                eA.functor.whiskerLeft Λ.π ≫ eA.functor.rightUnitor.hom)
                              eA.inverse ≫
                            eA.unitIso.inv).app
      x✝)

Tactic:
dsimp

Goal state after:
A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A'
eA : A' ≌ A
eC : C' ≌ C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x✝ : A'
⊢ Epi
    (𝟙 (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
      eA.unitIso.hom.app (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
        𝟙 (eA.inverse.obj (eA.functor.obj (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
          𝟙 (eA.inverse.obj (eA.functor.obj (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
            eA.inverse.map (e.hom.app (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
              𝟙 (eA.inverse.obj (ι.obj (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
                eA.inverse.map (𝟙 (ι.obj (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
                  eA.inverse.map (ι.map (𝟙 (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
                    eA.inverse.map
                        (ι.map
                          (𝟙 (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
                            eC.counitIso.hom.app (Λ.F.obj (eA.functor.obj x✝)) ≫ 𝟙 (Λ.F.obj (eA.functor.obj x✝)))) ≫
                      eA.inverse.map
                          (𝟙 (ι.obj (Λ.F.obj (eA.functor.obj x✝))) ≫
                            Λ.π.app (eA.functor.obj x✝) ≫ 𝟙 (eA.functor.obj x✝)) ≫
                        eA.unitIso.inv.app x✝)