Module: Mathlib.CategoryTheory.Functor.RegularEpi

Goal state before:
pp: case refine_1
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 Y : WalkingParallelPair} (f_1 : X ⟶ Y),
    (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map f_1 ≫
        (WalkingParallelPair.casesOn Y
            (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
          f_1

Tactic:
rintro _ _ (_ | _)

Goal state after:
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

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

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