-- Module: Mathlib.Algebra.Homology.LeftResolution.Transport
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst_2 : Category.{v_3, u_4} C'
inst_3 : Category.{v_4, u_3} A'
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
ι' : Functor.{v_3, v_4, u_4, u_3} C' A'
eA : Equivalence.{v_4, v_2, u_3, u_1} A' A
eC : Equivalence.{v_3, v_1, u_4, u_2} C' C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x : A'
dsimp :
  Epi (Y := x)
    (𝟙 (ι'.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)
⊢ Epi (Y := obj.{v_4, v_4, u_3, u_3} (𝟭 A') x)
    (NatTrans.app
      (((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)
      x)

Tactic:
dsimp