awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
zero : lift s ≫ t.π.app WalkingParallelPair.zero = s.π.app WalkingParallelPair.zero
⊢ lift s ≫ t.π.app j = s.π.app j
have one : lift s ≫ t.π.app one = s.π.app one
Tactic: cases j
Cleared hypotheses: j
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l : A ⟶ K // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
⊢ m = (fun {x : C} (k : x ⟶ X) (hk : k ≫ f = 0) ↦ (↑(h k hk) : x ⟶ K)) k hk
have rw : m ≫ i = (fun {x : C} (k : x ⟶ X) (hk : k ≫ f = 0) ↦ (↑(h k hk) : x ⟶ K)) k hk ≫ i
Tactic: rw [← cancel_mono i, (h k hk).2, hm]
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l : A ⟶ K // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
rw : m ≫ i = (fun {x : C} (k : x ⟶ X) (hk : k ≫ f = 0) ↦ (↑(h k hk) : x ⟶ K)) k hk ≫ i
rw₁ : m ≫ i = k
⊢ m = (fun {x : C} (k : x ⟶ X) (hk : k ≫ f = 0) ↦ (↑(h k hk) : x ⟶ K)) k hk
have rw₂ : k = k
Tactic: rw [← cancel_mono i, (h k hk).2, hm]
-- 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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
⊢ s.ι ≫ f = s.ι ≫ 0
have rw : (s.ι ≫ f) ≫ g = (s.ι ≫ 0) ≫ g
Tactic: rw [← cancel_mono g]
-- 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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m = (↑l : s'.pt ⟶ c.pt)
have apply : m ≫ Fork.ι c = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c
Tactic: apply Fork.IsLimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m ≫ Fork.ι c = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c
have hm₁ : m ≫ Fork.ι c = s.ι
Tactic: rw [Fork.ι_ofι] at hm
Cleared hypotheses: hm
-- 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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m ≫ Fork.ι c = s.ι
⊢ m ≫ Fork.ι c = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c
have rw : s.ι = (↑l : s'.pt ⟶ c.pt) ≫ Fork.ι c
Tactic: rw [hm]
-- 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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ f = Fork.ι s ≫ 0
have rw : Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g
Tactic: rw [← cancel_mono g, Category.assoc, ← hh]
-- 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
W : C
g : Y ⟶ W
h_1 : X ⟶ W
c : KernelFork h_1
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h_1
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m = (fun (s : Fork f 0) ↦ (i.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ c.pt)) s
have apply : m ≫ Fork.ι c = (fun (s : Fork f 0) ↦ (i.lift (KernelFork.ofι s.ι sorry) : (KernelFork.ofι s.ι sorry).pt ⟶ c.pt)) s ≫ Fork.ι c
Tactic: apply Fork.IsLimit.hom_ext i
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
hf : f = 0
⊢ 𝟙 X ≫ f = 0
have rw : Eq.{v + 1} (α := X ⟶ Y) (𝟙 X ≫ 0) 0
Tactic: rw [hf, 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
hf : f = 0
rw : Eq.{v + 1} (α := X ⟶ Y) (𝟙 X ≫ 0) 0
⊢ 𝟙 X ≫ f = 0
have rw₁ : Eq.{v + 1} (α := X ⟶ Y) 0 0
Tactic: rw [hf, 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero.{v, u} c.pt
s : KernelFork f
⊢ (fun (x : KernelFork f) ↦ (0 : x.pt ⟶ c.pt)) s ≫ Fork.ι c = Fork.ι s
have rw : 0 = Fork.ι s
Tactic: rw [zero_comp, ← cancel_mono f, zero_comp, s.condition]
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero.{v, u} c.pt
s : KernelFork f
rw : 0 = Fork.ι s
⊢ (fun (x : KernelFork f) ↦ (0 : x.pt ⟶ c.pt)) s ≫ Fork.ι c = Fork.ι s
have rw₁ : 0 ≫ f = Fork.ι s ≫ f
Tactic: rw [zero_comp, ← cancel_mono f, zero_comp, s.condition]
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero.{v, u} c.pt
s : KernelFork f
rw : 0 = Fork.ι s
rw₁ : 0 ≫ f = Fork.ι s ≫ f
⊢ (fun (x : KernelFork f) ↦ (0 : x.pt ⟶ c.pt)) s ≫ Fork.ι c = Fork.ι s
have rw₂ : 0 = Fork.ι s ≫ f
Tactic: rw [zero_comp, ← cancel_mono f, zero_comp, s.condition]
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero.{v, u} c.pt
s : KernelFork f
rw : 0 = Fork.ι s
rw₁ : 0 ≫ f = Fork.ι s ≫ f
rw₂ : 0 = Fork.ι s ≫ f
⊢ (fun (x : KernelFork f) ↦ (0 : x.pt ⟶ c.pt)) s ≫ Fork.ι c = Fork.ι s
have rw₃ : Eq.{v + 1} (α := s.pt ⟶ Y) 0 0
Tactic: rw [zero_comp, ← cancel_mono f, zero_comp, s.condition]
-- 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_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W' : C
s : W' ⟶ X'
hs : s ≫ g' = 0
⊢ (s ≫ e.inv) ≫ g = 0
have rw : (s ≫ e.inv) ≫ e.hom ≫ g' = 0
Tactic: rw [iff, Category.assoc, Iso.inv_hom_id_assoc, hs]
-- 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_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W' : C
s : W' ⟶ X'
hs : s ≫ g' = 0
rw : (s ≫ e.inv) ≫ e.hom ≫ g' = 0
⊢ (s ≫ e.inv) ≫ g = 0
have rw₁ : s ≫ e.inv ≫ e.hom ≫ g' = 0
Tactic: rw [iff, Category.assoc, Iso.inv_hom_id_assoc, hs]
-- 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_1 Y_1 : C
f : X_1 ⟶ Y_1
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W' : C
s : W' ⟶ X'
hs : s ≫ g' = 0
rw : (s ≫ e.inv) ≫ e.hom ≫ g' = 0
rw₁ : s ≫ e.inv ≫ e.hom ≫ g' = 0
rw₂ : s ≫ g' = 0
⊢ (s ≫ e.inv) ≫ g = 0
have rw₃ : Eq.{v + 1} (α := W' ⟶ Y') 0 0
Tactic: rw [iff, Category.assoc, Iso.inv_hom_id_assoc, hs]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
⊢ IsZero.{v, u} c.pt
have this : Mono (Fork.ι c)
Tactic: have := Fork.IsLimit.mono hc
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
⊢ IsZero.{v, u} c.pt
have rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
⊢ IsZero.{v, u} c.pt
have rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
⊢ IsZero.{v, u} c.pt
have rw₂ : (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
rw₂ : (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
⊢ IsZero.{v, u} c.pt
have rw₃ : 𝟙 c.pt ≫ Fork.ι c ≫ f = (0 ≫ Fork.ι c) ≫ f
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
rw₂ : (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₃ : 𝟙 c.pt ≫ Fork.ι c ≫ f = (0 ≫ Fork.ι c) ≫ f
⊢ IsZero.{v, u} c.pt
have rw₄ : 𝟙 c.pt ≫ Fork.ι c ≫ f = 0 ≫ Fork.ι c ≫ f
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
rw₂ : (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₃ : 𝟙 c.pt ≫ Fork.ι c ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₄ : 𝟙 c.pt ≫ Fork.ι c ≫ f = 0 ≫ Fork.ι c ≫ f
⊢ IsZero.{v, u} c.pt
have rw₅ : Eq.{v + 1} (α := c.pt ⟶ Y) (𝟙 c.pt ≫ 0) (CategoryStruct.comp (Y := c.pt) 0 0)
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
rw₂ : (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₃ : 𝟙 c.pt ≫ Fork.ι c ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₄ : 𝟙 c.pt ≫ Fork.ι c ≫ f = 0 ≫ Fork.ι c ≫ f
rw₅ : Eq.{v + 1} (α := c.pt ⟶ Y) (𝟙 c.pt ≫ 0) (CategoryStruct.comp (Y := c.pt) 0 0)
⊢ IsZero.{v, u} c.pt
have rw₆ : Eq.{v + 1} (α := c.pt ⟶ Y) 0 (CategoryStruct.comp (Y := c.pt) 0 0)
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
c : KernelFork f
hc : IsLimit c
inst_2 : Mono f
this : Mono (Fork.ι c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι c
rw₂ : (𝟙 c.pt ≫ Fork.ι c) ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₃ : 𝟙 c.pt ≫ Fork.ι c ≫ f = (0 ≫ Fork.ι c) ≫ f
rw₄ : 𝟙 c.pt ≫ Fork.ι c ≫ f = 0 ≫ Fork.ι c ≫ f
rw₅ : Eq.{v + 1} (α := c.pt ⟶ Y) (𝟙 c.pt ≫ 0) (CategoryStruct.comp (Y := c.pt) 0 0)
rw₆ : Eq.{v + 1} (α := c.pt ⟶ Y) 0 (CategoryStruct.comp (Y := c.pt) 0 0)
⊢ IsZero.{v, u} c.pt
have rw₇ : Eq.{v + 1} (α := c.pt ⟶ Y) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]
-- 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
inst_2 : HasKernel f
W : C
h : Eq (α := W ⟶ Y) (0 ≫ f) 0
⊢ Eq (α := W ⟶ kernel f) (lift f 0 h) 0
have h₁ : CategoryStruct.comp (Y := equalizer f 0) (lift f 0 h) (equalizer.ι f 0) =
  CategoryStruct.comp (Y := equalizer f 0) 0 (equalizer.ι f 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
k : W ⟶ X
h : k ≫ f = 0
inst_3 : Mono k
Z : C
g g' : Z ⟶ W
w : Eq (α := Z ⟶ kernel f) (g ≫ lift f k h) (g' ≫ lift f k h)
⊢ g = g'
have w₁ : CategoryStruct.comp (Y := kernel f) (g ≫ lift f k h) (ι f) = CategoryStruct.comp (Y := kernel f) (g' ≫ lift f k h) (ι f)
Tactic: replace w := w =≫ kernel.ι f
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
k : W ⟶ X
h : k ≫ f = 0
inst_3 : Mono k
Z : C
g g' : Z ⟶ W
w :
  CategoryStruct.comp (Y := kernel f) (g ≫ lift f k h) (ι f) =
    CategoryStruct.comp (Y := kernel f) (g' ≫ lift f k h) (ι f)
⊢ g = g'
have w₁ : g ≫ k = g' ≫ k
Tactic: simp only [Category.assoc, kernel.lift_ι] at w
Cleared hypotheses: 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 Z X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : HasKernel g
w : f ≫ g = 0
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
inst_3 : HasKernel g'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ Eq (α := X ⟶ kernel g') (CategoryStruct.comp (Y := kernel g) (lift g f w) (map g g' q r h₂)) (p ≫ lift g' f' w')
have h : CategoryStruct.comp (Y := equalizer g' 0) (CategoryStruct.comp (Y := kernel g) (lift g f w) (map g g' q r h₂))
    (equalizer.ι g' 0) =
  CategoryStruct.comp (Y := equalizer g' 0) (p ≫ lift g' f' w') (equalizer.ι g' 0)
Tactic: ext
-- 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
inst_2 : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasKernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
⊢ f' ≫ q.inv = p.inv ≫ f
have refine : (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom
Tactic: refine (cancel_mono q.hom).1 ?_
-- 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
⊢ Eq.{v + 1} (α := X ⟶ kernel.{v, u} (X := X) (Y := Y) 0) (Iso.inv kernelZeroIsoSource) (kernel.lift 0 (𝟙 X) ⋯)
have h : Eq.{v + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := equalizer.{v, u} (X := X) (Y := Y) 0 0) (Iso.inv kernelZeroIsoSource) (equalizer.ι 0 0))
  (CategoryStruct.comp (Y := equalizer.{v, u} (X := X) (Y := Y) 0 0) (kernel.lift 0 (𝟙 X) sorry) (equalizer.ι 0 0))
Tactic: ext
-- 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_1 : X ⟶ Y
inst_2 : HasKernel f_1
f g : X ⟶ Y
inst_3 : HasKernel f
inst_4 : HasKernel g
h : f = g
⊢ parallelPair f 0 ≅ parallelPair g 0
have rw : parallelPair g 0 ≅ parallelPair g 0
Tactic: rw [h]
-- 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
inst_2 : HasKernel f
h : f = f
⊢ kernelIsoOfEq h = Iso.refl (kernel f)
have w : CategoryStruct.comp (Y := equalizer f 0) (Iso.hom (kernelIsoOfEq h)) (equalizer.ι f 0) =
  Iso.hom (Iso.refl (kernel f)) ≫ equalizer.ι f 0
Tactic: ext
-- 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 g : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernel g
h : f = g
⊢ Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel g) (Iso.hom (kernelIsoOfEq h)) (kernel.ι g)) (kernel.ι f)
have subst : ∀ [inst_4 : HasKernel f],
  Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.hom (kernelIsoOfEq sorry)) (kernel.ι f)) (kernel.ι f)
Tactic: subst h
Cleared hypotheses: g, inst_3, h
-- 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 g : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernel g
h : f = g
⊢ Eq (α := kernel g ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.inv (kernelIsoOfEq h)) (kernel.ι f)) (kernel.ι g)
have subst : ∀ [inst_4 : HasKernel f],
  Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.inv (kernelIsoOfEq sorry)) (kernel.ι f)) (kernel.ι f)
Tactic: subst h
Cleared hypotheses: g, inst_3, h
-- 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 Z : C
f g : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ Eq (α := Z ⟶ kernel g) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.hom (kernelIsoOfEq h)))
    (kernel.lift g e ⋯)
have subst : ∀ [inst_4 : HasKernel f],
  Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.hom (kernelIsoOfEq sorry)))
    (kernel.lift f e sorry)
Tactic: subst h
Cleared hypotheses: g, inst_3, h
-- 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 Z : C
f g : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel g) (kernel.lift g e he) (Iso.inv (kernelIsoOfEq h)))
    (kernel.lift f e ⋯)
have refl : ∀ [inst_4 : HasKernel f] (he : e ≫ f = 0),
  Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.inv (kernelIsoOfEq sorry)))
    (kernel.lift f e sorry)
Tactic: cases h
Cleared hypotheses: g, inst_3, h, he
-- 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 g h : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernel g
inst_4 : HasKernel h
w₁ : f = g
w₂ : g = h
⊢ Eq (α := kernel f ≅ kernel h) (Iso.trans (Y := kernel g) (kernelIsoOfEq w₁) (kernelIsoOfEq w₂)) (kernelIsoOfEq ⋯)
have refl : ∀ [inst_5 : HasKernel f] (w₂ : f = h),
  Eq (α := kernel f ≅ kernel h) (Iso.trans (Y := kernel f) (kernelIsoOfEq sorry) (kernelIsoOfEq w₂)) (kernelIsoOfEq sorry)
Tactic: cases w₁
Cleared hypotheses: g, inst_3, w₁, 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasKernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasKernel f
inst_4 : Mono g
⊢ Eq (α := kernel (f ≫ g) ⟶ Y) (kernel.ι (f ≫ g) ≫ f) 0
have rw : Eq (α := kernel (f ≫ g) ⟶ Z) ((kernel.ι (f ≫ g) ≫ f) ≫ g) (0 ≫ g)
Tactic: rw [← cancel_mono g]
-- 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasKernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : IsIso f
inst_4 : HasKernel g
s : KernelFork (f ≫ g)
m : s.pt ⟶ kernel g
w : m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = (fun (s : KernelFork (f ≫ g)) ↦ (kernel.lift g (Fork.ι s ≫ f) ⋯ : s.pt ⟶ kernel g)) s
have simp_rw : m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) sorry)) ≫ f) sorry
Tactic: simp_rw [← 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasKernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : IsIso f
inst_4 : HasKernel g
s : KernelFork (f ≫ g)
m : s.pt ⟶ kernel g
w : m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯
have h : m ≫ equalizer.ι g 0 =
  CategoryStruct.comp (Y := equalizer g 0)
    (kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) sorry)) ≫ f) sorry) (equalizer.ι g 0)
Tactic: apply equalizer.hom_ext
-- 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
inst_2 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
⊢ CategoryStruct.comp (Y := Cone.pt (F := parallelPair f 0) (zeroKernelFork f))
      ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt (F := parallelPair f 0) (zeroKernelFork f))) s)
      (Fork.ι (zeroKernelFork f)) =
    s.ι
have rw : 0 = s.ι
Tactic: rw [zero_comp]
-- 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
inst_2 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
⊢ 0 = s.ι
have refine : s.ι ≫ f = 0
Tactic: refine (zero_of_comp_mono f ?_).symm