-- Module: Mathlib.CategoryTheory.Functor.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
this : IsRegularEpi (f.app k)
refine_1 :
  ∀ {X Y : WalkingParallelPair} (f_1 : X ⟶ Y),
    Eq (α :=
      (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj X ⟶
        (parallelPair
                (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                    pullback.isLimit (f.app k) (f.app k)).fst
                (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                    pullback.isLimit (f.app k) (f.app k)).snd ⋙
              obj (evaluation C D) k).obj
          Y)
      ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).map f_1 ≫
        Iso.hom
          (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
            (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj x ≅
              (parallelPair
                      (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                          pullback.isLimit (f.app k) (f.app k)).fst
                      (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                          pullback.isLimit (f.app k) (f.app k)).snd ⋙
                    obj (evaluation C D) k).obj
                x)
            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))))
      (Iso.hom
          (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
            (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj x ≅
              (parallelPair
                      (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                          pullback.isLimit (f.app k) (f.app k)).fst
                      (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                          pullback.isLimit (f.app k) (f.app k)).snd ⋙
                    obj (evaluation C D) k).obj
                x)
            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))) ≫
        (parallelPair
                (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                    pullback.isLimit (f.app k) (f.app k)).fst
                (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                    pullback.isLimit (f.app k) (f.app k)).snd ⋙
              obj (evaluation C D) k).map
          f_1)
⊢ parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd ≅
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k

Tactic:
refine NatIso.ofComponents (by rintro (_ | _); exacts [Iso.refl _, Iso.refl _]) ?_

Premises used: CategoryTheory.NatIso.ofComponents