Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: case refine_1.left
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)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map
        WalkingParallelPairHom.left ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one
          (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))).hom =
    (WalkingParallelPair.casesOn 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.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))).hom ≫
      (parallelPair
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).fst
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).snd ⋙
            (evaluation C D).obj k).map
        WalkingParallelPairHom.left

pp: case refine_1.right
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)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map
        WalkingParallelPairHom.right ≫
      (WalkingParallelPair.casesOn WalkingParallelPair.one
          (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))).hom =
    (WalkingParallelPair.casesOn 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.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))).hom ≫
      (parallelPair
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).fst
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).snd ⋙
            (evaluation C D).obj k).map
        WalkingParallelPairHom.right

pp: case refine_1.id
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)
X✝ : WalkingParallelPair
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map
        (WalkingParallelPairHom.id 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))).hom =
    (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))).hom ≫
      (parallelPair
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).fst
              (PullbackCone.combine f f (fun k ↦ pullback.cone (f.app k) (f.app k)) fun k ↦
                  pullback.isLimit (f.app k) (f.app k)).snd ⋙
            (evaluation C D).obj k).map
        (WalkingParallelPairHom.id X✝)

Tactic:
all_goals cat_disch

Goal state after: