-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst_1 : HasPullback f g
inst_2 : HasPullback f (a₁ ≫ g)
refine_1 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.snd f g) ≫ g = (s.snd ≫ pullback.snd f g) ≫ g
refine_2 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    (s.fst ≫ pullback.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯ ≫ a₁ ≫ g
refine_3 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g))
          (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯))
        ((fun (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)) ↦
            (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯)
                ⋯ :
              s.pt ⟶ pullback f (a₁ ≫ g)))
          s)
        (PullbackCone.fst
          (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯)) =
      s.fst
refine_4 :
  ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)),
    CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g))
          (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯))
        ((fun (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)) ↦
            (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯)
                ⋯ :
              s.pt ⟶ pullback f (a₁ ≫ g)))
          s)
        (PullbackCone.snd
          (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯)) =
      s.snd
⊢ IsKernelPair (R := pullback f (a₁ ≫ g)) (X := pullback f g) (pullback.fst f g)
    (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
have refine_5 : ∀ (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g))
  (m : s.pt ⟶ pullback f (a₁ ≫ g))
  (hm :
    ∀ (j : WalkingCospan),
      m ≫
          NatTrans.app
            (Cone.π
              (PullbackCone.mk (W := pullback f (a₁ ≫ g)) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) sorry sorry)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
            j =
        s.π.app j),
  m =
    (fun (s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)) ↦
        (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) sorry) sorry :
          s.pt ⟶ pullback f (a₁ ≫ g)))
      s
Tactic: refine ⟨⟨by rw [pullback.lift_fst, pullback.lift_fst]⟩, ⟨PullbackCone.isLimitAux _
    (fun s => pullback.lift (s.fst ≫ pullback.fst _ _)
      (h.lift (s.fst ≫ pullback.snd _ _) (s.snd ≫ pullback.snd _ _) ?_ ) ?_) (fun s => ?_)
        (fun s => ?_) (fun s (m : _ ⟶ pullback f (a₁ ≫ g)) hm => ?_)⟩⟩