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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasKernel f_1
X Y : C
f g : X ⟶ Y
inst_3 : HasKernel f
inst_4 : HasKernel g
h : f = g
⊢ Eq (α := kernel f ⟶ Y) (ι f ≫ 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasKernel f_1
X Y : C
f g : X ⟶ Y
inst_3 : HasKernel f
inst_4 : HasKernel g
h : f = g
⊢ Eq (α := kernel g ⟶ Y) (ι g ≫ f) 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 : Mono f
inst_3 : HasKernel f
⊢ IsZero.{v, u} (kernel f)

Tactic:
KernelFork.IsLimit.isZero_of_mono (c := KernelFork.ofι _ (kernel.condition f))
    (kernelIsKernel f)

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono, CategoryTheory.Limits.limit, CategoryTheory.Limits.kernelIsKernel
-- 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 : HasZeroObject.{v, u} C
⊢ Eq (α := Cone.pt (F := parallelPair f 0) (zeroKernelFork f) ⟶ X) (Fork.ι (zeroKernelFork f)) 0

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, 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 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
rw : 0 = s.ι
⊢ 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.ι

Tactic:
rw [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- 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 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
⊢ 0 = s.ι

Tactic:
(zero_of_comp_mono f ?_).symm

Premises used: CategoryTheory.Limits.zero_of_comp_mono, Eq.symm
-- 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 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
refine : s.ι ≫ f = 0
⊢ 0 = s.ι

Tactic:
refine (zero_of_comp_mono f ?_).symm

Premises used: CategoryTheory.Limits.zero_of_comp_mono, Eq.symm
-- 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 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
⊢ s.ι ≫ f = 0

Tactic:
KernelFork.condition _

Premises used: CategoryTheory.Limits.KernelFork.condition
-- 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 : HasZeroObject.{v, u} C
inst_3 : Mono f
s : Fork f 0
⊢ s.ι ≫ f = 0

Tactic:
exact KernelFork.condition _

Premises used: CategoryTheory.Limits.KernelFork.condition
-- 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 : HasZeroObject.{v, u} C
inst_3 : HasKernel f
inst_4 : Mono f
⊢ Eq (α := kernel f ⟶ X) (ι f) 0

Tactic:
zero_of_source_iso_zero _ (kernel.ofMono f)

Premises used: CategoryTheory.Limits.zero_of_source_iso_zero, CategoryTheory.Limits.kernel.ofMono
-- 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 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
⊢ Eq (α := 0 ⟶ Y) (0 ≫ 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
rw :
  Eq.{v + 1} (α := s.pt ⟶ X)
    (CategoryStruct.comp (Y := Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))
      ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s)
      (Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯)))
    0
rw₁ rw₂ : Eq.{v + 1} (α := s.pt ⟶ X) 0 0
⊢ CategoryStruct.comp (Y := Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))
      ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s)
      (Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯)) =
    s.ι

Tactic:
rw [hf _ _ (KernelFork.condition s), zero_comp]

Premises used: CategoryTheory.Limits.KernelFork.condition, CategoryTheory.Limits.zero_comp
-- 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 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
m : s.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯)
h : m ≫ Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯) = s.ι
dsimp : m = 0
⊢ m = (fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s

Tactic:
dsimp
-- 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 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
m : s.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯)
h : m ≫ Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯) = s.ι
⊢ m = 0

Tactic:
apply HasZeroObject.to_zero_ext

Premises used: CategoryTheory.Limits.HasZeroObject.to_zero_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
X' Y' : C
f' : X' ⟶ Y'
s : KernelFork f
hs : IsLimit s
s' : KernelFork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : e.hom ≫ Fork.ι s' = Fork.ι s ≫ eX.hom
⊢ (parallelPair f 0).map WalkingParallelPairHom.right ≫ eY.hom =
    eX.hom ≫ (parallelPair f' 0).map WalkingParallelPairHom.right

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'
s : KernelFork f
hs : IsLimit s
s' : KernelFork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : e.hom ≫ Fork.ι s' = Fork.ι s ≫ eX.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ((Cone.postcompose α.hom).obj s).π.app zero = e.hom ≫ s'.π.app zero

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
X' Y' : C
f' : X' ⟶ Y'
s : KernelFork f
hs : IsLimit s
s' : KernelFork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : e.hom ≫ Fork.ι s' = Fork.ι s ≫ eX.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ((Cone.postcompose α.hom).obj s).π.app one = e.hom ≫ s'.π.app one

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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
s : KernelFork f
hs : IsLimit s
⊢ Fork.ι s ≫ l = 0

Tactic:
simp [← i.comp_inv_eq.2 h.symm]

Premises used: Iff.mpr, CategoryTheory.Iso.comp_inv_eq, Eq.symm
-- 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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
s_1 : KernelFork f
hs : IsLimit s_1
s : Fork l 0
⊢ s.ι ≫ f = 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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
s_1 : KernelFork f
hs : IsLimit s_1
s : Fork l 0
⊢ CategoryStruct.comp (Y := Cone.pt (F := parallelPair l 0) (KernelFork.ofι (Fork.ι s_1) ⋯))
      ((fun (s : Fork l 0) ↦ (hs.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ s_1.pt)) s)
      (Fork.ι (KernelFork.ofι (Fork.ι s_1) ⋯)) =
    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 Y : C
f : X ⟶ Y
Z : C
l : X ⟶ Z
i : Z ≅ Y
h_1 : l ≫ i.hom = f
s_1 : KernelFork f
hs : IsLimit s_1
s : Fork l 0
m : s.pt ⟶ Cone.pt (F := parallelPair l 0) (KernelFork.ofι (Fork.ι s_1) ⋯)
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s_1) ⋯) = s.ι
apply :
  m ≫ Fork.ι s_1 =
    (fun (s : Fork l 0) ↦ (hs.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ s_1.pt)) s ≫ Fork.ι s_1
⊢ m = (fun (s : Fork l 0) ↦ (hs.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ s_1.pt)) s

Tactic:
apply Fork.IsLimit.hom_ext hs

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h_1 : l ≫ i.hom = f
s_1 : KernelFork f
hs : IsLimit s_1
s : Fork l 0
m : s.pt ⟶ Cone.pt (F := parallelPair l 0) (KernelFork.ofι (Fork.ι s_1) ⋯)
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s_1) ⋯) = s.ι
⊢ m ≫ Fork.ι s_1 =
    (fun (s : Fork l 0) ↦ (hs.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ s_1.pt)) s ≫ Fork.ι s_1

Tactic:
simpa using 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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
⊢ Eq (α := kernel f ⟶ Z) (ι f ≫ l) 0

Tactic:
simp [← i.comp_inv_eq.2 h.symm]

Premises used: Iff.mpr, CategoryTheory.Iso.comp_inv_eq, Eq.symm
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ l ≫ f = 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
j : WalkingParallelPair
zero :
  s.π.app WalkingParallelPair.zero = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) WalkingParallelPair.zero
one : s.π.app WalkingParallelPair.one = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) WalkingParallelPair.one
⊢ s.π.app j = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) j

Tactic:
cases j
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app zero = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) zero

Tactic:
(Iso.eq_inv_comp i).2 h

Premises used: Iff.mpr, CategoryTheory.Iso.eq_inv_comp
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app zero = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) zero

Tactic:
exact (Iso.eq_inv_comp i).2 h

Premises used: Iff.mpr, CategoryTheory.Iso.eq_inv_comp
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
one : s.π.app WalkingParallelPair.one = i.inv ≫ l ≫ f
⊢ s.π.app WalkingParallelPair.one = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) WalkingParallelPair.one

Tactic:
dsimp
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
one : s.π.app WalkingParallelPair.one = i.inv ≫ (i.hom ≫ Fork.ι s) ≫ f
⊢ s.π.app WalkingParallelPair.one = i.inv ≫ l ≫ f

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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.inv ≫ (i.hom ≫ Fork.ι s) ≫ 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 : X ⟶ Y
inst_2 : HasKernel f
Z : C
l : Z ⟶ X
i : Z ≅ kernel f
h : i.hom ≫ ι f = l
⊢ l ≫ f = 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
⊢ 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
s : CokernelCofork f
rw : Eq (α := X ⟶ s.pt) (0 ≫ Cofork.π s) 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
⊢ f ≫ Cofork.π s = 0

Tactic:
rw [Cofork.condition, zero_comp]

Premises used: CategoryTheory.Limits.Cofork.condition, CategoryTheory.Limits.zero_comp
-- 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
s : CokernelCofork f
⊢ s.ι.app zero = 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
Z : C
π : Y ⟶ Z
w : f ≫ π = 0
rw : Eq (α := X ⟶ Z) 0 (0 ≫ π)
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ Z) 0 0
⊢ f ≫ π = 0 ≫ π

Tactic:
rw [w, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y P : C
f : X ⟶ Y
π : Y ⟶ P
w : f ≫ π = 0
⊢ Cofork.π (ofπ π w) = π

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- 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
s : Cofork f 0
j : WalkingParallelPair
zero : s.ι.app WalkingParallelPair.zero ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π ⋯).ι.app WalkingParallelPair.zero
one : s.ι.app WalkingParallelPair.one ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π ⋯).ι.app WalkingParallelPair.one
⊢ s.ι.app j ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π ⋯).ι.app j

Tactic:
cases j
-- 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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
rw : f ≫ π = 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ P) 0 0
⊢ f ≫ π' = 0

Tactic:
rw [← h, 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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
j : WalkingParallelPair
zero :
  (CokernelCofork.ofπ π w).ι.app WalkingParallelPair.zero ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
    NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' ⋯)) WalkingParallelPair.zero
one :
  (CokernelCofork.ofπ π w).ι.app WalkingParallelPair.one ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
    NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' ⋯)) WalkingParallelPair.one
⊢ (CokernelCofork.ofπ π w).ι.app j ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
    NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' ⋯)) j

Tactic:
cases j
-- 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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
j : WalkingParallelPair
zero : t.ι.app WalkingParallelPair.zero ≫ desc s = s.ι.app WalkingParallelPair.zero
one : t.ι.app WalkingParallelPair.one ≫ desc s = s.ι.app WalkingParallelPair.one
⊢ t.ι.app j ≫ desc s = s.ι.app j

Tactic:
cases j
-- 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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app zero ≫ desc s = s.ι.app zero

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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app one ≫ desc s = s.ι.app one

Tactic:
fac s

Premises used: CategoryTheory.Limits.Cofork.π
-- 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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app one ≫ desc s = s.ι.app one

Tactic:
exact fac s
-- 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
X Y Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l : Q ⟶ A // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
rw : p ≫ m = p ≫ (fun {x : C} (k : Y ⟶ x) (hk : f ≫ k = 0) ↦ (↑(h k hk) : Q ⟶ x)) k hk
rw₁ : p ≫ m = k
rw₂ rw₃ : k = k
⊢ m = (fun {x : C} (k : Y ⟶ x) (hk : f ≫ k = 0) ↦ (↑(h k hk) : Q ⟶ x)) k hk

Tactic:
rw [← cancel_epi p, (h k hk).2, hm]

Premises used: CategoryTheory.cancel_epi, Subtype.property
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
rw : (g ≫ f) ≫ Cofork.π c = 0
⊢ h ≫ Cofork.π c = 0

Tactic:
rw [hh]
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
⊢ (g ≫ f) ≫ Cofork.π c = 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
a : g ≫ f ≫ s.π = g ≫ 0 ≫ s.π
⊢ f ≫ s.π = 0 ≫ s.π

Tactic:
apply hg.left_cancellation

Premises used: CategoryTheory.Epi.left_cancellation
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
a : 0 ≫ s.π = g ≫ 0 ≫ s.π
⊢ g ≫ f ≫ s.π = g ≫ 0 ≫ s.π

Tactic:
rw [← Category.assoc, ← hh, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.condition
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ 0 ≫ s.π = g ≫ 0 ≫ 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 Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m = s.π
apply : Cofork.π c ≫ m = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)
⊢ m = (↑l : c.pt ⟶ s'.pt)

Tactic:
apply Cofork.IsColimit.hom_ext i

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m = s.π
⊢ Cofork.π c ≫ m = s.π

Tactic:
rw [Cofork.π_ofπ] at hm

Premises used: CategoryTheory.Limits.Cofork.π_ofπ
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m = s.π
rw : s.π = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)
⊢ Cofork.π c ≫ m = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)

Tactic:
rw [hm]
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m = s.π
⊢ s.π = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)

Tactic:
l.2.symm

Premises used: CategoryTheory.Limits.Cofork.ofπ, Eq.symm, CategoryTheory.Limits.parallelPair, Subtype.property, CategoryTheory.Limits.Cofork.π
-- 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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m = s.π
⊢ s.π = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)

Tactic:
exact l.2.symm

Premises used: Eq.symm, Subtype.property