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
    (𝟙 (ι'.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✝)

Tactic:
;

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✝)