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)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
      WalkingParallelPair.zero ≅
    (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).obj
      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)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
      WalkingParallelPair.one ≅
    (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).obj
      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)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
      WalkingParallelPair.zero ≅
    (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).obj
      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)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
      WalkingParallelPair.one ≅
    (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).obj
      WalkingParallelPair.one