awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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)
rw₇ rw₈ : Eq.{v + 1} (α := c.pt ⟶ Y) 0 0
⊢ IsZero.{v, u} c.pt

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.KernelFork.condition, CategoryTheory.cancel_mono, CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf' : IsLimit kf'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ (Fork.ι kf ≫ Arrow.Hom.left φ) ≫ f' = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf' : IsLimit kf'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ kf.mapOfIsLimit hf' φ ≫ Fork.ι kf' = Fork.ι kf ≫ Arrow.Hom.left φ

Tactic:
hf'.fac _ _

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.KernelFork.mapOfIsLimit, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf : IsLimit kf
hf' : IsLimit kf'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ (kf.mapOfIsLimit hf' φ.hom ≫ kf'.mapOfIsLimit hf φ.inv) ≫ Fork.ι kf = 𝟙 kf.pt ≫ Fork.ι kf

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf : IsLimit kf
hf' : IsLimit kf'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ (kf'.mapOfIsLimit hf φ.inv ≫ kf.mapOfIsLimit hf' φ.hom) ≫ Fork.ι kf' = 𝟙 kf'.pt ≫ Fork.ι kf'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ Eq (α := equalizer f 0 ⟶ X) (equalizer.ι f 0) (kernel.ι f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ Eq (α := kernel f ⟶ Y) (ι f ≫ f) 0

Tactic:
KernelFork.condition _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.KernelFork.condition, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ Iso.hom (Iso.refl (limit.cone (parallelPair f 0)).pt) ≫ Fork.ι (Fork.ofι (P := kernel f) (kernel.ι f) ⋯) =
    Fork.ι (limit.cone (parallelPair f 0))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ CategoryStruct.comp (Y := kernel f) (lift f k h) (ι f) = k

Tactic:
(kernelIsKernel f).fac (KernelFork.ofι k h) WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.limit, CategoryTheory.Limits.kernelIsKernel, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
h₁ :
  CategoryStruct.comp (Y := equalizer f 0) (lift f 0 h) (equalizer.ι f 0) =
    CategoryStruct.comp (Y := equalizer f 0) 0 (equalizer.ι f 0)
⊢ Eq (α := W ⟶ kernel f) (lift f 0 h) 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ CategoryStruct.comp (Y := equalizer f 0) (lift f 0 h) (equalizer.ι f 0) =
    CategoryStruct.comp (Y := equalizer f 0) 0 (equalizer.ι f 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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)
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 ≫ k = g' ≫ k

Tactic:
simp only [Category.assoc, kernel.lift_ι] at w

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 : g ≫ k = g' ≫ k
⊢ g = g'

Tactic:
(cancel_mono k).1 w

Premises used: CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 : g ≫ k = g' ≫ k
⊢ g = g'

Tactic:
exact (cancel_mono k).1 w

Premises used: CategoryTheory.cancel_mono, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 = p ≫ f'
⊢ Eq (α := kernel f ⟶ Y') ((ι f ≫ p) ≫ f') 0

Tactic:
simp [← w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 = p ≫ f'
inst_4 : IsIso p
inst_5 : Mono q
⊢ Eq (α := kernel f' ⟶ Y) ((kernel.ι f' ≫ inv p) ≫ f) 0

Tactic:
simp [← cancel_mono q, w]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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'
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)
⊢ Eq (α := X ⟶ kernel g') (CategoryStruct.comp (Y := kernel g) (lift g f w) (map g g' q r h₂)) (p ≫ lift g' f' w')

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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'
⊢ 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:
simp [h₁]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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

Tactic:
(cancel_mono q.hom).1 ?_

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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'
refine : (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom
⊢ f' ≫ q.inv = p.inv ≫ f

Tactic:
refine (cancel_mono q.hom).1 ?_

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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) ≫ q.hom = (p.inv ≫ f) ≫ q.hom

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ IsIso.{v, u} (C := C) (X := kernel.{v, u} (X := X) (Y := Y) 0) (ι 0)

Tactic:
equalizer.ι_of_self _

Premises used: CategoryTheory.Limits.equalizer.ι_of_self
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
inst_3 : Epi (X := kernel f) (kernel.ι f)
⊢ Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) (kernel.ι f ≫ 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := kernel.{v, u} (X := X) (Y := Y) 0 ⟶ X) (Iso.hom kernelZeroIsoSource) (kernel.ι 0)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ Eq.{v + 1} (α := X ⟶ Y) (𝟙 X ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
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) ⋯) (equalizer.ι 0 0))
⊢ Eq.{v + 1} (α := X ⟶ kernel.{v, u} (X := X) (Y := Y) 0) (Iso.inv kernelZeroIsoSource) (kernel.lift 0 (𝟙 X) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
⊢ 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) ⋯) (equalizer.ι 0 0))

Tactic:
simp [kernelZeroIsoSource]

Premises used: CategoryTheory.Limits.kernelZeroIsoSource
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
rw rw₁ : parallelPair g 0 ≅ parallelPair g 0
⊢ parallelPair f 0 ≅ parallelPair g 0

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
w :
  CategoryStruct.comp (Y := equalizer f 0) (Iso.hom (kernelIsoOfEq h)) (equalizer.ι f 0) =
    Iso.hom (Iso.refl (kernel f)) ≫ equalizer.ι f 0
⊢ kernelIsoOfEq h = Iso.refl (kernel f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ CategoryStruct.comp (Y := equalizer f 0) (Iso.hom (kernelIsoOfEq h)) (equalizer.ι f 0) =
    Iso.hom (Iso.refl (kernel f)) ≫ equalizer.ι f 0

Tactic:
simp [kernelIsoOfEq]

Premises used: CategoryTheory.Limits.kernelIsoOfEq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
subst :
  ∀ [inst_4 : HasKernel f],
    Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.hom (kernelIsoOfEq ⋯)) (kernel.ι f)) (kernel.ι f)
⊢ Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel g) (Iso.hom (kernelIsoOfEq h)) (kernel.ι g)) (kernel.ι f)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 inst_3 : HasKernel f
⊢ Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.hom (kernelIsoOfEq ⋯)) (kernel.ι f)) (kernel.ι f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
subst :
  ∀ [inst_4 : HasKernel f],
    Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.inv (kernelIsoOfEq ⋯)) (kernel.ι f)) (kernel.ι f)
⊢ Eq (α := kernel g ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.inv (kernelIsoOfEq h)) (kernel.ι f)) (kernel.ι g)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 inst_3 : HasKernel f
⊢ Eq (α := kernel f ⟶ X) (CategoryStruct.comp (Y := kernel f) (Iso.inv (kernelIsoOfEq ⋯)) (kernel.ι f)) (kernel.ι f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
Z : C
f g : X ⟶ Y
inst_3 : HasKernel f
inst_4 : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ e ≫ g = 0

Tactic:
simp [← h, he]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
subst :
  ∀ [inst_4 : HasKernel f],
    Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.hom (kernelIsoOfEq ⋯)))
      (kernel.lift f e ⋯)
⊢ Eq (α := Z ⟶ kernel g) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.hom (kernelIsoOfEq h)))
    (kernel.lift g e ⋯)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_2 : HasKernel f
e : Z ⟶ X
he : e ≫ f = 0
inst_3 : HasKernel f
⊢ Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.hom (kernelIsoOfEq ⋯)))
    (kernel.lift f e ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
Z : C
f g : X ⟶ Y
inst_3 : HasKernel f
inst_4 : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ e ≫ f = 0

Tactic:
simp [h, he]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
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 ⋯)))
      (kernel.lift f e ⋯)
⊢ Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel g) (kernel.lift g e he) (Iso.inv (kernelIsoOfEq h)))
    (kernel.lift f e ⋯)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_2 : HasKernel f
e : Z ⟶ X
inst_3 : HasKernel f
he : e ≫ f = 0
⊢ Eq (α := Z ⟶ kernel f) (CategoryStruct.comp (Y := kernel f) (kernel.lift f e he) (Iso.inv (kernelIsoOfEq ⋯)))
    (kernel.lift f e ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
refl :
  ∀ [inst_5 : HasKernel f] (w₂ : f = h),
    Eq (α := kernel f ≅ kernel h) (Iso.trans (Y := kernel f) (kernelIsoOfEq ⋯) (kernelIsoOfEq w₂)) (kernelIsoOfEq ⋯)
⊢ Eq (α := kernel f ≅ kernel h) (Iso.trans (Y := kernel g) (kernelIsoOfEq w₁) (kernelIsoOfEq w₂)) (kernelIsoOfEq ⋯)

Tactic:
cases w₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f h : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasKernel h
inst_4 : HasKernel f
w₂ : f = h
⊢ Eq (α := kernel f ≅ kernel h) (Iso.trans (Y := kernel f) (kernelIsoOfEq ⋯) (kernelIsoOfEq w₂)) (kernelIsoOfEq ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 : f ≠ 0
⊢ ¬Epi (X := kernel f) (kernel.ι f)

Tactic:
fun _ =>
  w (eq_zero_of_epi_kernel f)

Premises used: CategoryTheory.Limits.eq_zero_of_epi_kernel, Not
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 : f ≠ 0
⊢ IsIso (X := kernel f) (kernel.ι f) → False

Tactic:
fun _ =>
  kernel_not_epi_of_nonzero w inferInstance

Premises used: CategoryTheory.Limits.kernel_not_epi_of_nonzero, inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
inst_3 : HasKernel f
g : Y ⟶ Z
inst_4 : Mono g
⊢ HasKernel (f ≫ g)

Tactic:
⟨⟨{   cone := _
        isLimit := isKernelCompMono (limit.isLimit _) g rfl }⟩⟩

Premises used: CategoryTheory.Limits.isKernelCompMono._proof_1, CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.limit.cone, Nonempty.intro, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.LimitCone.mk, OfNat.ofNat, CategoryTheory.Limits.isKernelCompMono, CategoryTheory.Limits.parallelPair, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
rw : Eq (α := kernel (f ≫ g) ⟶ Z) ((kernel.ι (f ≫ g) ≫ f) ≫ g) (0 ≫ g)
⊢ Eq (α := kernel (f ≫ g) ⟶ Y) (kernel.ι (f ≫ g) ≫ f) 0

Tactic:
rw [← cancel_mono g]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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) ⟶ Z) ((kernel.ι (f ≫ g) ≫ f) ≫ g) (0 ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 ⟶ Z) (kernel.ι f ≫ f ≫ g) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ Eq (α := kernel g ⟶ Z) ((kernel.ι g ≫ inv f) ≫ f ≫ g) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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)
⊢ (Fork.ι s ≫ f) ≫ g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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)),
    CategoryStruct.comp (Y :=
        Cone.pt (F := parallelPair (f ≫ g) 0) (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯))
        ((fun (s : KernelFork (f ≫ g)) ↦ (kernel.lift g (Fork.ι s ≫ f) ⋯ : s.pt ⟶ kernel g)) s)
        (Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯)) =
      Fork.ι s

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
simp_rw : m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯
⊢ m = (fun (s : KernelFork (f ≫ g)) ↦ (kernel.lift g (Fork.ι s ≫ f) ⋯ : s.pt ⟶ kernel g)) s

Tactic:
simp_rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
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) ⋯)) ≫ f) ⋯) (equalizer.ι g 0)
⊢ m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯

Tactic:
apply equalizer.hom_ext

Premises used: CategoryTheory.Limits.equalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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 ≫ equalizer.ι g 0 =
    CategoryStruct.comp (Y := equalizer g 0)
      (kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (Z := kernel g) (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯) (equalizer.ι g 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
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
⊢ Eq (α := kernel (f ≫ g) ⟶ Z) ((kernel.ι (f ≫ g) ≫ f) ≫ g) 0

Tactic:
simp