-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.RegularEpi (goal)
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)
⊢ 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
have 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)
Tactic: refine NatIso.ofComponents (by rintro (_ | _); exacts [Iso.refl _, Iso.refl _]) ?_