awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
zero_1 : (X Y : C) → Zero (X ⟶ Y)
comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
mk : @comp_zero ≍ @comp_zero_1
mk₁ : zero_comp ≍ zero_comp_1
⊢ { zero := zero, comp_zero := @comp_zero, zero_comp := zero_comp : HasZeroMorphisms.{v, u} C } =
    { zero := zero_1, comp_zero := @comp_zero_1, zero_comp := zero_comp_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
zero_1 : (X Y : C) → Zero (X ⟶ Y)
comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
⊢ @comp_zero ≍ @comp_zero_1

Tactic:
apply proof_irrel_heq

Premises used: proof_irrel_heq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
zero : (X Y : C) → Zero (X ⟶ Y)
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
zero_1 : (X Y : C) → Zero (X ⟶ Y)
comp_zero_1 : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), Eq (α := X ⟶ Z) (f ≫ 0) 0
zero_comp_1 : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), Eq (α := X ⟶ Z) (0 ≫ f) 0
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
this : Eq (α := (X Y : C) → Zero (X ⟶ Y)) HasZeroMorphisms.zero HasZeroMorphisms.zero
⊢ zero_comp ≍ zero_comp_1

Tactic:
apply proof_irrel_heq

Premises used: proof_irrel_heq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
w : ∀ (X Y : C), Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero
⊢ I = J

Tactic:
apply ext_aux

Premises used: _private.0.CategoryTheory.Limits.HasZeroMorphisms.ext_aux
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero

Tactic:
apply I.zero_comp X (J.zero Y Y).zero

Premises used: Zero.zero, CategoryTheory.Limits.HasZeroMorphisms.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero

Tactic:
have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by
    apply I.zero_comp X (J.zero Y Y).zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
this : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero

Tactic:
apply J.comp_zero (I.zero X Y).zero Y

Premises used: Zero.zero, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
this : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
⊢ Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero

Tactic:
have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
    apply J.comp_zero (I.zero X Y).zero Y
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
I J : HasZeroMorphisms.{v, u} C
X Y : C
this : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
that : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
w : Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero) Zero.zero
w₁ w₂ :
  Eq.{v + 1} (α := X ⟶ Y) (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero)
    (CategoryStruct.comp (Y := Y) Zero.zero Zero.zero)
⊢ Eq.{v + 1} (α := X ⟶ Y) Zero.zero Zero.zero

Tactic:
rw [← this, ← that]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
⊢ Subsingleton (HasZeroMorphisms.{v, u} C)

Tactic:
⟨ext⟩

Premises used: CategoryTheory.Limits.HasZeroMorphisms.ext, Subsingleton.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := op Y ⟶ op X) (Quiver.Hom.op 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : Cᵒᵖ
⊢ Eq.{v + 1} (α := unop Y ⟶ unop X) (Quiver.Hom.unop 0) 0

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : Mono g
h : f ≫ g = 0
⊢ f = 0

Tactic:
rw [← zero_comp, cancel_mono] at h

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : Mono g
h_1 : f ≫ g = 0
h : f = 0
⊢ f = 0

Tactic:
h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : Mono g
h_1 : f ≫ g = 0
h : f = 0
⊢ f = 0

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : Epi f
h : f ≫ g = 0
⊢ g = 0

Tactic:
rw [← comp_zero, cancel_epi] at h

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : Epi f
h_1 : f ≫ g = 0
h : g = 0
⊢ g = 0

Tactic:
h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : Epi f
h_1 : f ≫ g = 0
h : g = 0
⊢ g = 0

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
w : Eq (α := image f ⟶ Y) (image.ι f) 0
rw : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) = 0
rw₁ : Eq (α := X ⟶ Y) (CategoryStruct.comp (Y := image f) (factorThruImage f) 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ f = 0

Tactic:
rw [← image.fac f, w, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.Limits.image.fac, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasImage f
w : f ≠ 0
⊢ Ne (α := image f ⟶ Y) (image.ι f) 0

Tactic:
fun h => w (eq_zero_of_image_eq_zero h)

Premises used: CategoryTheory.Limits.eq_zero_of_image_eq_zero, Not
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
X Y : Functor.{v, v', u, u'} C D
η : X ⟶ Y
H : Functor.{v, v', u, u'} C D
w : ∀ (X_1 : C), Eq (α := X.obj X_1 ⟶ H.obj X_1) (NatTrans.app (η ≫ 0) X_1) (NatTrans.app 0 X_1)
⊢ Eq (α := X ⟶ H) (η ≫ 0) 0

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
H : Functor.{v, v', u, u'} C D
X : C
w : Eq (α := X_1.obj X ⟶ H.obj X) (η.app X ≫ NatTrans.app 0 X) (NatTrans.app 0 X)
⊢ Eq (α := X_1.obj X ⟶ H.obj X) (NatTrans.app (η ≫ 0) X) (NatTrans.app 0 X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
X_1 Y : Functor.{v, v', u, u'} C D
η : X_1 ⟶ Y
H : Functor.{v, v', u, u'} C D
X : C
⊢ Eq (α := X_1.obj X ⟶ H.obj X) (η.app X ≫ NatTrans.app 0 X) (NatTrans.app 0 X)

Tactic:
apply comp_zero

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
F G H : Functor.{v, v', u, u'} C D
η : G ⟶ H
w : ∀ (X : C), Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app (0 ≫ η) X) (NatTrans.app 0 X)
⊢ Eq (α := F ⟶ H) (0 ≫ η) 0

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
F G H : Functor.{v, v', u, u'} C D
η : G ⟶ H
X : C
w : Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app 0 X ≫ η.app X) (NatTrans.app 0 X)
⊢ Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app (0 ≫ η) X) (NatTrans.app 0 X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
F G H : Functor.{v, v', u, u'} C D
η : G ⟶ H
X : C
⊢ Eq (α := F.obj X ⟶ H.obj X) (NatTrans.app 0 X ≫ η.app X) (NatTrans.app 0 X)

Tactic:
apply zero_comp

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v', u'} D
F G : Functor.{v, v', u, u'} C D
j : C
⊢ Eq.{v' + 1} (α := F.obj j ⟶ G.obj j) (NatTrans.app 0 j) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
o : IsZero.{v, u} X
f : X ⟶ Y
⊢ f = 0

Tactic:
o.eq_of_src _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
o : IsZero.{v, u} Y
f : X ⟶ Y
⊢ f = 0

Tactic:
o.eq_of_tgt _ _

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Y : C
f : X ⟶ Y
rw : Eq.{v + 1} (α := X ⟶ Y) 0 default
⊢ f = default

Tactic:
rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, OfNat.ofNat, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Y : C
f : X ⟶ Y
⊢ Eq.{v + 1} (α := X ⟶ Y) 0 default

Tactic:
simp only
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Y : C
f : Y ⟶ X
rw : Eq.{v + 1} (α := Y ⟶ X) 0 default
⊢ f = default

Tactic:
rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X : C
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Y : C
f : Y ⟶ X
⊢ Eq.{v + 1} (α := Y ⟶ X) 0 default

Tactic:
simp only
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ Y) (𝟙 X ≫ 0) (CategoryStruct.comp (Y := X) 0 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ Y) (0 ≫ 𝟙 Y) (CategoryStruct.comp (Y := Y) 0 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
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
h : f = 0
⊢ Mono.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsZero.{v, u} X

Tactic:
apply of_mono_zero X Y

Premises used: CategoryTheory.Limits.IsZero.of_mono_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : Epi f
h : f = 0
⊢ Epi.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
inst_2 : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsZero.{v, u} Y

Tactic:
apply of_epi_zero X Y

Premises used: CategoryTheory.Limits.IsZero.of_epi_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ↔ f = 0
⊢ IsZero.{v, u} X ↔ f = 0

Tactic:
rw [iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
mp : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 → f = 0
mpr : f = 0 → Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ↔ f = 0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
mp : 𝟙 X ≫ f = 0
mp₁ : Eq (α := X ⟶ Y) (0 ≫ f) 0
mp₂ mp₃ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ f = 0

Tactic:
rw [← Category.id_comp f, h, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : f = 0
mpr : f ≫ retraction f = 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
rw [← IsSplitMono.id f]

Premises used: CategoryTheory.IsSplitMono.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
h : f = 0
⊢ f ≫ retraction f = 0

Tactic:
simp only [h, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
rw : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ↔ f = 0
⊢ IsZero.{v, u} Y ↔ f = 0

Tactic:
rw [iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
mp : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → f = 0
mpr : f = 0 → Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ↔ f = 0

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
h : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
mp : f ≫ 𝟙 Y = 0
mp₁ : Eq (α := X ⟶ Y) (f ≫ 0) 0
mp₂ mp₃ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ f = 0

Tactic:
rw [← Category.comp_id f, h, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
h : f = 0
mpr : section_ f ≫ f = 0
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0

Tactic:
rw [← IsSplitEpi.id f]

Premises used: CategoryTheory.IsSplitEpi.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
h : f = 0
⊢ section_ f ≫ f = 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
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
i : IsZero.{v, u} Y
⊢ Mono.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
obtain rfl := i.eq_zero_of_tgt f

Premises used: CategoryTheory.Limits.IsZero.eq_zero_of_tgt, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsZero.{v, u} Y
inst_2 : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsZero.{v, u} X

Tactic:
IsZero.of_mono_zero X Y

Premises used: CategoryTheory.Limits.IsZero.of_mono_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsZero.{v, u} Y
inst_2 : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsZero.{v, u} X

Tactic:
exact IsZero.of_mono_zero X Y

Premises used: CategoryTheory.Limits.IsZero.of_mono_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : Epi f
i : IsZero.{v, u} X
⊢ Epi.{v, u} (C := C) (X := X) (Y := Y) 0

Tactic:
obtain rfl := i.eq_zero_of_src f

Premises used: CategoryTheory.Limits.IsZero.eq_zero_of_src, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsZero.{v, u} X
inst_2 : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsZero.{v, u} Y

Tactic:
IsZero.of_epi_zero X Y

Premises used: CategoryTheory.Limits.IsZero.of_epi_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsZero.{v, u} X
inst_2 : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ IsZero.{v, u} Y

Tactic:
exact IsZero.of_epi_zero X Y

Premises used: CategoryTheory.Limits.IsZero.of_epi_zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y : C
f : X ⟶ Y
Z : C
change : f ≫ hO.from_ Y ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z
⊢ Eq (α := X ⟶ Z) (f ≫ 0) 0

Tactic:
change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z

Premises used: CategoryTheory.Limits.IsZero.to_, CategoryTheory.Limits.IsZero.from_, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y : C
f : X ⟶ Y
Z : C
rw : (f ≫ hO.from_ Y) ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z
⊢ f ≫ hO.from_ Y ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y : C
f : X ⟶ Y
Z : C
e_a : f ≫ hO.from_ Y = hO.from_ X
⊢ (f ≫ hO.from_ Y) ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ hO.from_ Y = hO.from_ X

Tactic:
apply hO.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y Z : C
f : Y ⟶ Z
change : (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
⊢ Eq (α := X ⟶ Z) (0 ≫ f) 0

Tactic:
change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z

Premises used: CategoryTheory.Limits.IsZero.to_, CategoryTheory.Limits.IsZero.from_, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y Z : C
f : Y ⟶ Z
rw : hO.from_ X ≫ hO.to_ Y ≫ f = hO.from_ X ≫ hO.to_ Z
⊢ (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y Z : C
f : Y ⟶ Z
e_a : hO.to_ Y ≫ f = hO.to_ Z
⊢ hO.from_ X ≫ hO.to_ Y ≫ f = hO.from_ X ≫ hO.to_ Z

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
O : C
hO : IsZero.{v, u} O
X Y Z : C
f : Y ⟶ Z
⊢ hO.to_ Y ≫ f = hO.to_ Z

Tactic:
apply hO.eq_of_src

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
change :
  Eq (α := X ⟶ Z) (f ≫ CategoryStruct.comp (Y := 0) default default) (CategoryStruct.comp (Y := 0) default default)
⊢ Eq (α := X ⟶ Z) (f ≫ 0) 0

Tactic:
change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default

Premises used: Inhabited.default
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
rw : Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) (f ≫ default) default) (CategoryStruct.comp (Y := 0) default default)
⊢ Eq (α := X ⟶ Z) (f ≫ CategoryStruct.comp (Y := 0) default default) (CategoryStruct.comp (Y := 0) default default)

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
e_a : Eq (α := X ⟶ 0) (f ≫ default) default
⊢ Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) (f ≫ default) default) (CategoryStruct.comp (Y := 0) default default)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := X ⟶ 0) (f ≫ default) default

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton