-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
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) ⋯ ⋯)
                  (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯))
              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) ⋯) ⋯ :
            s.pt ⟶ pullback f (a₁ ≫ g)))
        s
⊢ 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) ⋯ ⋯)

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 => ?_)⟩⟩