awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
have refine_3 : CategoryStruct.comp (Y := pullback 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) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
      ((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)
      (PullbackCone.fst
        (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)))
    (pullback.fst f g) =
  s.fst ≫ pullback.fst f g
Tactic: ext
-- 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)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
refine_3 :
  CategoryStruct.comp (Y := pullback 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) ⋯ ⋯) ⋯)))
      (pullback.fst f g) =
    s.fst ≫ 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
have refine_3₁ : CategoryStruct.comp (Y := pullback 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) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
      ((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)
      (PullbackCone.fst
        (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)))
    (pullback.snd f g) =
  s.fst ≫ pullback.snd f g
Tactic: ext
-- 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)
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
have refine_4 : CategoryStruct.comp (Y := pullback 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) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
      ((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)
      (PullbackCone.snd
        (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)))
    (pullback.fst f g) =
  s.snd ≫ pullback.fst f g
Tactic: ext
-- 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)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
refine_4 :
  CategoryStruct.comp (Y := pullback 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) ⋯ ⋯) ⋯)))
      (pullback.fst f g) =
    s.snd ≫ 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
have refine_4₁ : CategoryStruct.comp (Y := pullback 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) sorry sorry)
          (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) sorry sorry) sorry))
      ((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)
      (PullbackCone.snd
        (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)))
    (pullback.snd f g) =
  s.snd ≫ pullback.snd f g
Tactic: ext
-- 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)
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
have refine_5 : m ≫ pullback.fst f (a₁ ≫ g) =
  CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
    ((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)
    (pullback.fst f (a₁ ≫ g))
Tactic: apply pullback.hom_ext
-- 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)
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
refine_5 :
  m ≫ pullback.fst f (a₁ ≫ g) =
    CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
      ((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)
      (pullback.fst f (a₁ ≫ g))
⊢ 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
have refine_5₁ : m ≫ pullback.snd f (a₁ ≫ g) =
  CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
    ((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)
    (pullback.snd f (a₁ ≫ g))
Tactic: apply pullback.hom_ext
-- 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)
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 ≫ pullback.snd f (a₁ ≫ g) =
    CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
      ((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)
      (pullback.snd f (a₁ ≫ g))
have refine_5 : (m ≫ pullback.snd f (a₁ ≫ g)) ≫ (IsPullback.cone h).fst =
  CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
      ((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)
      (pullback.snd f (a₁ ≫ g)) ≫
    (IsPullback.cone h).fst
Tactic: apply PullbackCone.IsLimit.hom_ext h.isLimit
-- 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)
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
refine_5 :
  (m ≫ pullback.snd f (a₁ ≫ g)) ≫ (IsPullback.cone h).fst =
    CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
        ((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)
        (pullback.snd f (a₁ ≫ g)) ≫
      (IsPullback.cone h).fst
⊢ m ≫ pullback.snd f (a₁ ≫ g) =
    CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
      ((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)
      (pullback.snd f (a₁ ≫ g))
have refine_5₁ : (m ≫ pullback.snd f (a₁ ≫ g)) ≫ (IsPullback.cone h).snd =
  CategoryStruct.comp (Y := pullback f (a₁ ≫ g))
      ((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)
      (pullback.snd f (a₁ ≫ g)) ≫
    (IsPullback.cone h).snd
Tactic: apply PullbackCone.IsLimit.hom_ext h.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
⊢ Mono f
have obtain : ∀ (l : X ⟶ (IsPullback.cone h).pt) (h₁ : l ≫ (IsPullback.cone h).fst = 𝟙 X) (h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X),
  Mono f
Tactic: obtain ⟨l, h₁, h₂⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit (𝟙 _) (𝟙 _) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ (IsPullback.cone h).fst = 𝟙 X
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f
have h₃ : l = inv a
Tactic: rw [IsPullback.cone_fst, ← IsIso.eq_comp_inv, Category.id_comp] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f
have h₃ : (IsPullback.cone h).snd = a
Tactic: rw [h₁, IsIso.inv_comp_eq, Category.comp_id] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
⊢ Mono f
have right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ g₂ : Z ⟶ X
e : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
have right_cancellation : ∀ (l' : Z ⟶ (IsPullback.cone h).pt) (e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f),
  l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd
Tactic: obtain ⟨l', rfl, rfl⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit _ _ e
Cleared hypotheses: g₁, g₂, e
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
⊢ l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd
have right_cancellation : l' ≫ a = l' ≫ (IsPullback.cone h).snd
Tactic: rw [IsPullback.cone_fst, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
right_cancellation : l' ≫ a = l' ≫ (IsPullback.cone h).snd
⊢ l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd
have right_cancellation₁ : l' ≫ a = l' ≫ a
Tactic: rw [IsPullback.cone_fst, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
e : a = b
⊢ Mono f
have h₁ : IsKernelPair f a a
Tactic: induction e
Cleared hypotheses: h, e
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst_1 : Mono f
⊢ IsIso a
have rw : IsIso ((IsPullback.isLimit sorry).conePointUniqueUpToIso (IsPullback.isLimit h)).inv
Tactic: rw [←
    show _ = a from
      (Category.comp_id _).symm.trans
        ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
          WalkingCospan.left)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
⊢ IsPullback a a f f
have h : a = a ≫ 𝟙 X
Tactic: convert! (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _)⟩).paste_vert (IsKernelPair.id_of_mono f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.KernelPair (goal)
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst_1 : IsIso a
inst_2 : Mono f
h : a = a ≫ 𝟙 X
⊢ IsPullback a a f f
have h₁ : f = 𝟙 X ≫ f
Tactic: convert! (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _)⟩).paste_vert (IsKernelPair.id_of_mono f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ Fork.ι s ≫ f = 0
have rw : Eq (α := s.pt ⟶ Y) (Fork.ι s ≫ 0) 0
Tactic: rw [Fork.condition, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
s : KernelFork f
rw : Eq (α := s.pt ⟶ Y) (Fork.ι s ≫ 0) 0
⊢ Fork.ι s ≫ f = 0
have rw₁ : Eq.{v + 1} (α := s.pt ⟶ Y) 0 0
Tactic: rw [Fork.condition, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
⊢ ι ≫ f = ι ≫ 0
have rw : Eq (α := Z ⟶ Y) 0 (ι ≫ 0)
Tactic: rw [w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
rw : Eq (α := Z ⟶ Y) 0 (ι ≫ 0)
⊢ ι ≫ f = ι ≫ 0
have rw₁ : Eq.{v + 1} (α := Z ⟶ Y) 0 0
Tactic: rw [w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
rw : ι ≫ f = 0
⊢ ι' ≫ f = 0
have rw₁ : Eq.{v + 1} (α := P ⟶ Y) 0 0
Tactic: rw [← h, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app j = s.π.app j
have zero : lift s ≫ t.π.app zero = s.π.app zero
Tactic: cases j
Cleared hypotheses: j