awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
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.snd f g) =
    s.fst ≫ pullback.snd 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

Tactic:
ext
-- 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)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
⊢ 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

Tactic:
simp
-- 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)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
⊢ 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.snd f g) =
    s.fst ≫ pullback.snd f g

Tactic:
simp
-- 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)
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
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.snd f g) =
    s.snd ≫ pullback.snd 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

Tactic:
ext
-- 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)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
⊢ 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

Tactic:
simp [s.condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- 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)
s : PullbackCone (X := pullback f g) (Y := pullback f g) (pullback.fst f g) (pullback.fst f g)
⊢ 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.snd f g) =
    s.snd ≫ pullback.snd f g

Tactic:
simp
-- 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)
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))
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) ⋯) ⋯ :
            s.pt ⟶ pullback f (a₁ ≫ g)))
        s)
      (pullback.snd 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

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- 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)
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.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))

Tactic:
simpa using hm WalkingCospan.left =≫ pullback.fst f g

Premises used: CategoryTheory.Limits.pullback.fst, CategoryTheory.Limits.WalkingCospan.left
-- 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)
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
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) ⋯)
                ⋯ :
              s.pt ⟶ pullback f (a₁ ≫ g)))
          s)
        (pullback.snd f (a₁ ≫ g)) ≫
      (IsPullback.cone h).snd
⊢ 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))

Tactic:
apply PullbackCone.IsLimit.hom_ext h.isLimit

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, CategoryTheory.IsPullback.isLimit
-- 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)
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)) ≫ (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

Tactic:
simpa using hm WalkingCospan.left =≫ pullback.snd f g

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.WalkingCospan.left
-- 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)
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)) ≫ (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) ⋯)
                ⋯ :
              s.pt ⟶ pullback f (a₁ ≫ g)))
          s)
        (pullback.snd f (a₁ ≫ g)) ≫
      (IsPullback.cone h).snd

Tactic:
simpa using hm WalkingCospan.right =≫ pullback.snd f g

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.WalkingCospan.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
obtain :
  ∀ (l : X ⟶ (IsPullback.cone h).pt) (h₁ : l ≫ (IsPullback.cone h).fst = 𝟙 X) (h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X),
    Mono f
⊢ Mono f

Tactic:
obtain ⟨l, h₁, h₂⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit (𝟙 _) (𝟙 _) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.PullbackCone.IsLimit.lift', CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ l = inv a

Tactic:
rw [IsPullback.cone_fst, ← IsIso.eq_comp_inv, Category.id_comp] at h₁

Premises used: CategoryTheory.IsPullback.cone_fst, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
h₃ : l = inv a
⊢ l ≫ (IsPullback.cone h).snd = 𝟙 X

Tactic:
rw [IsPullback.cone_fst, ← IsIso.eq_comp_inv, Category.id_comp] at h₁

Premises used: CategoryTheory.IsPullback.cone_fst, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ (IsPullback.cone h).snd = a

Tactic:
rw [h₁, IsIso.inv_comp_eq, Category.comp_id] at h₂

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
⊢ Mono f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
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
⊢ g₁ = g₂

Tactic:
obtain ⟨l', rfl, rfl⟩ := Limits.PullbackCone.IsLimit.lift' h.isLimit _ _ e

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift', rfl, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
right_cancellation₁ right_cancellation₂ : l' ≫ a = l' ≫ a
⊢ l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd

Tactic:
rw [IsPullback.cone_fst, h₂]

Premises used: CategoryTheory.IsPullback.cone_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
h : IsKernelPair f a a
⊢ Mono f

Tactic:
⟨fun g₁ g₂ e ↦ (lift_fst h g₁ g₂ e).symm.trans <| lift_snd h g₁ g₂ e⟩

Premises used: CategoryTheory.IsKernelPair.lift_snd, CategoryTheory.Mono.mk, CategoryTheory.IsKernelPair.lift_fst, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
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
⊢ IsKernelPair f a a

Tactic:
induction e
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a a
⊢ Mono f

Tactic:
h.mono_of_eq_fst_snd'

Premises used: CategoryTheory.IsKernelPair.mono_of_eq_fst_snd'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair
Goal:
C : Type u
inst : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a a
⊢ Mono f

Tactic:
exact h.mono_of_eq_fst_snd'

Premises used: CategoryTheory.IsKernelPair.mono_of_eq_fst_snd'