Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: case zero
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).pt).hom =
    (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app WalkingParallelPair.zero

pp: case one
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).pt).hom =
    (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app WalkingParallelPair.one

Tactic:
;

Goal state after:
case zero
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).pt).hom =
    (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app WalkingParallelPair.zero

case one
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst✝² : HasPushouts D
inst✝¹ : IsRegularEpiCategory D
F G : C ⥤ D
f : F ⟶ G
inst✝ : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (NatIso.ofComponents
                      (fun X ↦
                        WalkingParallelPair.casesOn X
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.zero))
                          (Iso.refl
                            ((parallelPair (pullback.cone (f.app k) (f.app k)).fst
                                  (pullback.cone (f.app k) (f.app k)).snd).obj
                              WalkingParallelPair.one)))
                      ⋯).inv).obj
              (Cofork.ofπ (f.app k) ⋯)).pt).hom =
    (((evaluation C D).obj k).mapCocone (Cofork.ofπ f ⋯)).ι.app WalkingParallelPair.one