awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F : ExactFunctor.{v₁, v₂, u₁, u₂} C D
⊢ ObjectProperty.FullSubcategory.obj (P := additiveFunctor C D) (Functor.obj (ofExact C D) F) =
    F.obj (P := exactFunctor C D)

Tactic:
rfl

Premises used: CategoryTheory.exactFunctor, CategoryTheory.additiveFunctor, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F G : LeftExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ InducedCategory.Hom.hom (Functor.map (ofLeftExact C D) α) = α.hom

Tactic:
rfl

Premises used: CategoryTheory.leftExactFunctor, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F G : RightExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ InducedCategory.Hom.hom (Functor.map (ofRightExact C D) α) = α.hom

Tactic:
rfl

Premises used: rfl, CategoryTheory.rightExactFunctor
-- Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₁, u₁} C
inst_3 : Preadditive.{v₂, u₂} D
inst_4 : HasZeroObject.{v₁, u₁} C
inst_5 : HasZeroObject.{v₂, u₂} D
inst_6 : HasBinaryBiproducts.{v₁, u₁} C
F G : ExactFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
⊢ InducedCategory.Hom.hom (Functor.map (ofExact C D) α) = α.hom

Tactic:
rfl

Premises used: CategoryTheory.exactFunctor, CategoryTheory.additiveFunctor, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
h : ((x_3 + x_4) ≫ x_5).hom = (x_3 ≫ x_5 + x_4 ≫ x_5).hom
⊢ (x_3 + x_4) ≫ x_5 = x_3 ≫ x_5 + x_4 ≫ x_5

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ ((x_3 + x_4) ≫ x_5).hom = (x_3 ≫ x_5 + x_4 ≫ x_5).hom

Tactic:
apply add_comp

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
h : (x_3 ≫ (x_4 + x_5)).hom = (x_3 ≫ x_4 + x_3 ≫ x_5).hom
⊢ x_3 ≫ (x_4 + x_5) = x_3 ≫ x_4 + x_3 ≫ x_5

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
⊢ (x_3 ≫ (x_4 + x_5)).hom = (x_3 ≫ x_4 + x_3 ≫ x_5).hom

Tactic:
apply comp_add

Premises used: CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
F : D → C
X Y : InducedCategory C F
aesop_cat aesop_cat₁ aesop_cat₂ aesop_cat₃ :
  ∀ (x y : X ⟶ Y),
    Equiv.toFun InducedCategory.homEquiv (x + y) =
      Equiv.toFun InducedCategory.homEquiv x + Equiv.toFun InducedCategory.homEquiv y
⊢ ∀ (x y : X ⟶ Y),
    Equiv.toFun InducedCategory.homEquiv (x + y) =
      Equiv.toFun InducedCategory.homEquiv x + Equiv.toFun InducedCategory.homEquiv y

Tactic:
aesop_cat
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Z : ObjectProperty.{v, u} C
x x_1 x_2 : Z.FullSubcategory
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
h : ((x_3 + x_4) ≫ x_5).hom = (x_3 ≫ x_5 + x_4 ≫ x_5).hom
⊢ (x_3 + x_4) ≫ x_5 = x_3 ≫ x_5 + x_4 ≫ x_5

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Z : ObjectProperty.{v, u} C
x x_1 x_2 : Z.FullSubcategory
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ ((x_3 + x_4) ≫ x_5).hom = (x_3 ≫ x_5 + x_4 ≫ x_5).hom

Tactic:
apply add_comp

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Z : ObjectProperty.{v, u} C
x x_1 x_2 : Z.FullSubcategory
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
h : (x_3 ≫ (x_4 + x_5)).hom = (x_3 ≫ x_4 + x_3 ≫ x_5).hom
⊢ x_3 ≫ (x_4 + x_5) = x_3 ≫ x_4 + x_3 ≫ x_5

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Z : ObjectProperty.{v, u} C
x x_1 x_2 : Z.FullSubcategory
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
⊢ (x_3 ≫ (x_4 + x_5)).hom = (x_3 ≫ x_4 + x_3 ≫ x_5).hom

Tactic:
apply comp_add

Premises used: CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ (fun (g : Q ⟶ R) ↦ f ≫ g) (g + g') =
    HAdd.hAdd (α := P ⟶ R) ((fun (g : Q ⟶ R) ↦ f ≫ g) g) ((fun (g : Q ⟶ R) ↦ f ≫ g) g')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
g : Q ⟶ R
f f' : P ⟶ Q
⊢ (fun (f : P ⟶ Q) ↦ f ≫ g) (f + f') =
    HAdd.hAdd (α := P ⟶ R) ((fun (f : P ⟶ Q) ↦ f ≫ g) f) ((fun (f : P ⟶ Q) ↦ f ≫ g) f')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f f' : P ⟶ Q
g : Q ⟶ R
⊢ (f - f') ≫ g = f ≫ g - f' ≫ g

Tactic:
map_sub (rightComp P g) f f'

Premises used: map_sub, CategoryTheory.Preadditive.rightComp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ f ≫ (g - g') = f ≫ g - f ≫ g'

Tactic:
map_sub (leftComp R f) g g'

Premises used: map_sub, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ (-f) ≫ g = -f ≫ g

Tactic:
map_neg (rightComp P g) f

Premises used: map_neg, CategoryTheory.Preadditive.rightComp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ f ≫ (-g) = -f ≫ g

Tactic:
map_neg (leftComp R f) g

Premises used: map_neg, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
n : ℕ
⊢ (n • f) ≫ g = n • f ≫ g

Tactic:
map_nsmul (rightComp P g) n f

Premises used: CategoryTheory.Preadditive.rightComp, map_nsmul
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
n : ℕ
⊢ f ≫ (n • g) = n • f ≫ g

Tactic:
map_nsmul (leftComp R f) n g

Premises used: CategoryTheory.Preadditive.leftComp, map_nsmul
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
n : ℤ
⊢ (n • f) ≫ g = n • f ≫ g

Tactic:
map_zsmul (rightComp P g) n f

Premises used: CategoryTheory.Preadditive.rightComp, map_zsmul
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
n : ℤ
⊢ f ≫ (n • g) = n • f ≫ g

Tactic:
map_zsmul (leftComp R f) n g

Premises used: CategoryTheory.Preadditive.leftComp, map_zsmul
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (Q ⟶ R)
⊢ Eq (α := P ⟶ R) (f ≫ ∑ j ∈ s, g j) (∑ j ∈ s, f ≫ g j)

Tactic:
map_sum (leftComp R f) _ _

Premises used: map_sum, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
J : Type u_1
s : Finset J
f : J → (P ⟶ Q)
g : Q ⟶ R
⊢ Eq (α := P ⟶ R) ((∑ j ∈ s, f j) ≫ g) (∑ j ∈ s, f j ≫ g)

Tactic:
map_sum (rightComp P g) _ _

Premises used: map_sum, CategoryTheory.Preadditive.rightComp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R S : C
J : Type u_1
s : Finset J
f : J → (P ⟶ Q)
g : J → (Q ⟶ R)
h : R ⟶ S
simp : Eq (α := P ⟶ S) ((∑ j ∈ s, f j ≫ g j) ≫ h) (∑ j ∈ s, (f j ≫ g j) ≫ h)
⊢ Eq (α := P ⟶ S) ((∑ j ∈ s, f j ≫ g j) ≫ h) (∑ j ∈ s, f j ≫ g j ≫ h)

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R S : C
J : Type u_1
s : Finset J
f : J → (P ⟶ Q)
g : J → (Q ⟶ R)
h : R ⟶ S
⊢ Eq (α := P ⟶ S) ((∑ j ∈ s, f j ≫ g j) ≫ h) (∑ j ∈ s, (f j ≫ g j) ≫ h)

Tactic:
apply sum_comp

Premises used: CategoryTheory.Preadditive.sum_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Epi f
Z : C
g g' : Q ⟶ Z
H : (-f) ≫ g = (-f) ≫ g'
rwa : ∀ (H : -f ≫ g = (-f) ≫ g'), g = g'
rwa₁ : ∀ (H : -f ≫ g = -f ≫ g'), g = g'
rwa₂ : ∀ (H : f ≫ (-g) = -f ≫ g'), g = g'
rwa₃ : ∀ (H : f ≫ (-g) = f ≫ (-g')), g = g'
rwa₄ : ∀ (H : -g = -g'), g = g'
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (H : g = g'), g = g'
⊢ g = g'

Tactic:
rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H

Premises used: CategoryTheory.Preadditive.comp_neg, neg_inj, CategoryTheory.Preadditive.neg_comp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P_1 Q_1 R : C
f_1 f' : P_1 ⟶ Q_1
g_1 g'_1 : Q_1 ⟶ R
P Q : C
f : P ⟶ Q
inst_2 : Mono f
Z : C
g g' : Z ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
rwa : ∀ (H : -g ≫ f = g' ≫ (-f)), g = g'
rwa₁ : ∀ (H : -g ≫ f = -g' ≫ f), g = g'
rwa₂ : ∀ (H : (-g) ≫ f = -g' ≫ f), g = g'
rwa₃ : ∀ (H : (-g) ≫ f = (-g') ≫ f), g = g'
rwa₄ : ∀ (H : -g = -g'), g = g'
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (H : g = g'), g = g'
⊢ g = g'

Tactic:
rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.cancel_mono, neg_inj, CategoryTheory.Preadditive.neg_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
dsimp : Eq (α := End X) (f ≫ 0) 0
⊢ 0 * f = 0

Tactic:
dsimp [mul]

Premises used: AddMonoidHom.mul
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ Eq (α := End X) (f ≫ 0) 0

Tactic:
HasZeroMorphisms.comp_zero f _

Premises used: CategoryTheory.End, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ Eq (α := End X) (f ≫ 0) 0

Tactic:
exact HasZeroMorphisms.comp_zero f _

Premises used: CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
dsimp : Eq (α := End X) (0 ≫ f) 0
⊢ f * 0 = 0

Tactic:
dsimp [mul]

Premises used: AddMonoidHom.mul
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ Eq (α := End X) (0 ≫ f) 0

Tactic:
HasZeroMorphisms.zero_comp _ f

Premises used: CategoryTheory.End, CategoryTheory.Limits.HasZeroMorphisms.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f_1 f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ Eq (α := End X) (0 ≫ f) 0

Tactic:
exact HasZeroMorphisms.zero_comp _ f

Premises used: CategoryTheory.Limits.HasZeroMorphisms.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
Q R : C
f : Q ⟶ R
⊢ Mono f ↔ ∀ (P : C) (g : P ⟶ Q), g ≫ f = 0 → g = 0

Tactic:
⟨fun _ _ _ => zero_of_comp_mono _, mono_of_cancel_zero f⟩

Premises used: CategoryTheory.Limits.zero_of_comp_mono, CategoryTheory.Preadditive.mono_of_cancel_zero, Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasLimit (parallelPair f 0)
w : Eq (α := kernel f ⟶ X) (kernel.ι f) 0
P : C
g : P ⟶ X
h : g ≫ f = 0
rw : CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) (kernel.ι f) = 0
rw₁ : Eq (α := P ⟶ X) (CategoryStruct.comp (Y := kernel f) (kernel.lift f g h) 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := P ⟶ X) 0 0
⊢ g = 0

Tactic:
rw [← kernel.lift_ι f g h, w, Limits.comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero.{v, u} c.pt
P : C
g : P ⟶ X
hg : g ≫ f = 0
obtain : ∀ (a : P ⟶ c.pt) (ha : a ≫ Fork.ι c = g), g = 0
⊢ g = 0

Tactic:
obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero.{v, u} c.pt
P : C
g : P ⟶ X
hg : g ≫ f = 0
a : P ⟶ c.pt
ha : a ≫ Fork.ι c = g
rw : a ≫ Fork.ι c = 0
rw₁ : Eq (α := P ⟶ X) (0 ≫ Fork.ι c) 0
rw₂ rw₃ : Eq.{v + 1} (α := P ⟶ X) 0 0
⊢ g = 0

Tactic:
rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp]

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.Limits.zero_comp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
⊢ Mono f ↔ IsZero.{v, u} c.pt

Tactic:
⟨fun _ ↦ KernelFork.IsLimit.isZero_of_mono hc, mono_of_isZero_kernel' c hc⟩

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono, Iff.intro, CategoryTheory.Preadditive.mono_of_isZero_kernel'
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasKernel f
h : IsZero.{v, u} (kernel f)
⊢ Mono f

Tactic:
mono_of_isZero_kernel' _ (kernelIsKernel _) h

Premises used: CategoryTheory.Preadditive.mono_of_isZero_kernel', CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasKernel f
⊢ Mono f ↔ IsZero.{v, u} (kernel f)

Tactic:
mono_iff_isZero_kernel' _ (limit.isLimit _)

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Preadditive.mono_iff_isZero_kernel', CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q : C
f : P ⟶ Q
h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0
⊢ Epi f

Tactic:
⟨fun {Z} g g' hg =>
    sub_eq_zero.1 <| h _ <| (map_sub (leftComp Z f) g g').trans <| sub_eq_zero.2 hg⟩

Premises used: Iff.mpr, map_sub, sub_eq_zero, HSub.hSub, CategoryTheory.Epi.mk, Iff.mp, CategoryTheory.Preadditive.leftComp, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q : C
f : P ⟶ Q
⊢ Epi f ↔ ∀ (R : C) (g : Q ⟶ R), f ≫ g = 0 → g = 0

Tactic:
⟨fun _ _ _ => zero_of_epi_comp _, epi_of_cancel_zero f⟩

Premises used: CategoryTheory.Limits.zero_of_epi_comp, Iff.intro, CategoryTheory.Preadditive.epi_of_cancel_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasColimit (parallelPair f 0)
w : Eq (α := Y ⟶ cokernel f) (cokernel.π f) 0
R : C
g : Y ⟶ R
h : f ≫ g = 0
rw : CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (cokernel.desc f g h) = 0
rw₁ : Eq (α := Y ⟶ R) (CategoryStruct.comp (Y := cokernel f) 0 (cokernel.desc f g h)) 0
rw₂ rw₃ : Eq.{v + 1} (α := Y ⟶ R) 0 0
⊢ g = 0

Tactic:
rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero.{v, u} c.pt
R : C
g : Y ⟶ R
hg : f ≫ g = 0
obtain : ∀ (a : c.pt ⟶ R) (ha : Cofork.π c ≫ a = g), g = 0
⊢ g = 0

Tactic:
obtain ⟨a, ha⟩ := CokernelCofork.IsColimit.desc' hc _ hg

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
h : IsZero.{v, u} c.pt
R : C
g : Y ⟶ R
hg : f ≫ g = 0
a : c.pt ⟶ R
ha : Cofork.π c ≫ a = g
rw : Cofork.π c ≫ a = 0
rw₁ : Eq (α := Y ⟶ R) (Cofork.π c ≫ 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := Y ⟶ R) 0 0
⊢ g = 0

Tactic:
rw [← ha, h.eq_of_src a 0, Limits.comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.IsZero.eq_of_src, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
⊢ Epi f ↔ IsZero.{v, u} c.pt

Tactic:
⟨fun _ ↦ CokernelCofork.IsColimit.isZero_of_epi hc, epi_of_isZero_cokernel' c hc⟩

Premises used: Iff.intro, CategoryTheory.Preadditive.epi_of_isZero_cokernel', CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasCokernel f
h : IsZero.{v, u} (cokernel f)
⊢ Epi f

Tactic:
epi_of_isZero_cokernel' _ (cokernelIsCokernel _) h

Premises used: CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Preadditive.epi_of_isZero_cokernel'
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasCokernel f
⊢ Epi f ↔ IsZero.{v, u} (cokernel f)

Tactic:
epi_iff_isZero_cokernel' _ (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Preadditive.epi_iff_isZero_cokernel'
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_2 : IsIso f
rw : g = inv f ≫ 0 ↔ g = 0
rw₁ rw₂ : g = 0 ↔ g = 0
⊢ f ≫ g = 0 ↔ g = 0

Tactic:
rw [← IsIso.eq_inv_comp, Limits.comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.IsIso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_2 : IsIso g
rw : f = 0 ≫ inv g ↔ f = 0
rw₁ rw₂ : f = 0 ↔ f = 0
⊢ f ≫ g = 0 ↔ f = 0

Tactic:
rw [← IsIso.eq_comp_inv, Limits.zero_comp]

Premises used: CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : HasLimit (parallelPair f 0)
w : kernel f ≅ 0
⊢ Mono f

Tactic:
mono_of_kernel_zero (zero_of_source_iso_zero _ w)

Premises used: CategoryTheory.Limits.zero_of_source_iso_zero, CategoryTheory.Preadditive.mono_of_kernel_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : HasColimit (parallelPair f 0)
w : cokernel f ≅ 0
⊢ Epi f

Tactic:
epi_of_cokernel_zero (zero_of_target_iso_zero _ w)

Premises used: CategoryTheory.Preadditive.epi_of_cokernel_zero, CategoryTheory.Limits.zero_of_target_iso_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
rw : Fork.ι c ≫ f - Fork.ι c ≫ g = 0
rw₁ : Fork.ι c ≫ (f - g) = 0
rw₂ rw₃ : Eq.{v + 1} (α := c.pt ⟶ Y) 0 0
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g

Tactic:
rw [← sub_eq_zero, ← comp_sub, c.condition]

Premises used: sub_eq_zero, CategoryTheory.Limits.KernelFork.condition, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ (forkOfKernelFork c).ι = Fork.ι c

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.Fork.ι, CategoryTheory.Preadditive.forkOfKernelFork, CategoryTheory.Limits.parallelPair, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
rw : c.ι ≫ f - c.ι ≫ g = c.ι ≫ 0
rw₁ : c.ι ≫ f - c.ι ≫ g = 0
rw₂ : c.ι ≫ f = c.ι ≫ g
rw₃ rw₄ : c.ι ≫ g = c.ι ≫ g
⊢ c.ι ≫ (f - g) = c.ι ≫ 0

Tactic:
rw [comp_sub, comp_zero, sub_eq_zero, c.condition]

Premises used: sub_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.Fork.condition, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ Fork.ι (kernelForkOfFork c) = c.ι

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.Fork.ι, CategoryTheory.Preadditive.kernelForkOfFork, CategoryTheory.Limits.parallelPair, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ι ≫ (f - g) = 0

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ Eq (α := KernelFork (f - g)) (kernelForkOfFork (Fork.ofι ι w)) (KernelFork.ofι ι ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.Preadditive.kernelForkOfFork, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m : s.pt ⟶ (forkOfKernelFork c).pt
h : m ≫ (forkOfKernelFork c).ι = s.ι
apply : m ≫ Fork.ι c = i.lift (kernelForkOfFork s) ≫ Fork.ι c
⊢ m = i.lift (kernelForkOfFork s)

Tactic:
apply Fork.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext