awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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
⊢ f = 0
have mp₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
Tactic: rw [← Category.comp_id f, h, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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
⊢ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have mpr : section_ f ≫ f = 0
Tactic: rw [← IsSplitEpi.id f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
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
⊢ IsZero.{v, u} X
have inst : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: obtain rfl := i.eq_zero_of_tgt f
Cleared hypotheses: f, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
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
⊢ IsZero.{v, u} Y
have inst : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: obtain rfl := i.eq_zero_of_src f
Cleared hypotheses: f, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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
⊢ Eq (α := X ⟶ Z) (f ≫ 0) 0
have change : f ≫ hO.from_ Y ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z
Tactic: change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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.to_ Z = hO.from_ X ≫ hO.to_ Z
have rw : (f ≫ hO.from_ Y) ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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.to_ Z = hO.from_ X ≫ hO.to_ Z
have e_a : f ≫ hO.from_ Y = hO.from_ X
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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
⊢ Eq (α := X ⟶ Z) (0 ≫ f) 0
have change : (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
Tactic: change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
have rw : hO.from_ X ≫ hO.to_ Y ≫ f = hO.from_ X ≫ hO.to_ Z
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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.from_ X ≫ hO.to_ Y ≫ f = hO.from_ X ≫ hO.to_ Z
have e_a : hO.to_ Y ≫ f = hO.to_ Z
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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 ⟶ Z) (f ≫ 0) 0
have change : Eq (α := X ⟶ Z) (f ≫ CategoryStruct.comp (Y := 0) default default) (CategoryStruct.comp (Y := 0) default default)
Tactic: change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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 ⟶ Z) (f ≫ CategoryStruct.comp (Y := 0) default default) (CategoryStruct.comp (Y := 0) default default)
have rw : Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) (f ≫ default) default) (CategoryStruct.comp (Y := 0) default default)
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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 ⟶ Z) (CategoryStruct.comp (Y := 0) (f ≫ default) default) (CategoryStruct.comp (Y := 0) default default)
have e_a : Eq (α := X ⟶ 0) (f ≫ default) default
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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 Z : C
f : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) (0 ≫ f) 0
have change : Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default default ≫ f) (CategoryStruct.comp (Y := 0) default default)
Tactic: change ((default : X ⟶ 0) ≫ default) ≫ f = (default : X ⟶ 0) ≫ default
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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 Z : C
f : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default default ≫ f) (CategoryStruct.comp (Y := 0) default default)
have rw : Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default (default ≫ f)) (CategoryStruct.comp (Y := 0) default default)
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
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 Z : C
f : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) (CategoryStruct.comp (Y := 0) default (default ≫ f)) (CategoryStruct.comp (Y := 0) default default)
have e_a : Eq (α := 0 ⟶ Z) (default ≫ f) default
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = 0
have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
Tactic: have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv := by simp only [Iso.hom_inv_id, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = 0
have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
Tactic: have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
h_1 : g ≫ f = h ≫ f
⊢ g = h
have rw : 0 = h
Tactic: rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
h_1 : g ≫ f = h ≫ f
rw : 0 = h
⊢ g = h
have rw₁ : Eq.{v + 1} (α := Z ⟶ X) 0 0
Tactic: rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
h_1 : f ≫ g = f ≫ h
⊢ g = h
have rw : 0 = h
Tactic: rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
h_1 : f ≫ g = f ≫ h
rw : 0 = h
⊢ g = h
have rw₁ : Eq.{v + 1} (α := Y ⟶ Z) 0 0
Tactic: rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : Mono f
h : f = 0
⊢ X ≅ 0
have inst : Mono.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: subst h
Cleared hypotheses: f, inst_4, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_4 : Epi f
h : f = 0
⊢ Y ≅ 0
have inst : Epi.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: subst h
Cleared hypotheses: f, inst_4, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P : IsIsomorphic.{v, u} X 0
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X)
have have : ∀ (P : X ≅ 0), Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X)
Tactic: have P := P.some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X)
have rw : CategoryStruct.comp (Y := 0) 0 0 = P.hom ≫ 𝟙 0 ≫ P.inv
Tactic: rw [← P.hom_inv_id, ← Category.id_comp P.inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
⊢ CategoryStruct.comp (Y := 0) 0 0 = P.hom ≫ 𝟙 0 ≫ P.inv
have h : P.hom ≫ 𝟙 0 ≫ P.inv = CategoryStruct.comp (Y := 0) 0 0
Tactic: apply Eq.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
X : C
P_1 : IsIsomorphic.{v, u} X 0
P : X ≅ 0
⊢ P.hom ≫ 𝟙 0 ≫ P.inv = CategoryStruct.comp (Y := 0) 0 0
have h : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: simp only [id_comp, Iso.hom_inv_id, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have rw : Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
Tactic: rw [← IsIso.hom_inv_id (0 : X ⟶ Y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
i : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have rw : Eq.{v + 1} (α := X ⟶ X) (CategoryStruct.comp (Y := Y) 0 (inv 0)) 0 ∧
  Eq.{v + 1} (α := Y ⟶ Y) (CategoryStruct.comp (Y := X) (inv 0) 0) 0
Tactic: rw [← IsIso.inv_hom_id (0 : X ⟶ Y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 ≃ (X ≅ 0) × (Y ≅ 0)
have refine : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ≃ (X ≅ 0) × (Y ≅ 0)
Tactic: refine (isIsoZeroEquiv X Y).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 ≃ (X ≅ 0) × (Y ≅ 0)
have symm : (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
⊢ (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have toFun : ∀ (a : (X ≅ 0) × (Y ≅ 0)), Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
toFun : ∀ (a : (X ≅ 0) × (Y ≅ 0)), Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have invFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → (X ≅ 0) × (Y ≅ 0)
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
toFun : ∀ (a : (X ≅ 0) × (Y ≅ 0)), Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
invFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → (X ≅ 0) × (Y ≅ 0)
⊢ (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have left_inv : autoParam
  (Function.LeftInverse
    (fun (a : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
      And.casesOn (motive := fun (x : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        (X ≅ 0) × (Y ≅ 0)) a fun (hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0) (hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) hX, (idZeroEquivIsoZero Y : (a : 𝟙 Y = 0) → Y ≅ 0) hY))
    sorry)
  Equiv.left_inv._autoParam
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
toFun : ∀ (a : (X ≅ 0) × (Y ≅ 0)), Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
invFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0 → (X ≅ 0) × (Y ≅ 0)
left_inv :
  autoParam
    (Function.LeftInverse
      (fun (a : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        And.casesOn (motive := fun (x : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
          (X ≅ 0) × (Y ≅ 0)) a fun (hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0) (hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
          ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) hX, (idZeroEquivIsoZero Y : (a : 𝟙 Y = 0) → Y ≅ 0) hY))
      ⋯)
    Equiv.left_inv._autoParam
⊢ (X ≅ 0) × (Y ≅ 0) ≃ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have right_inv : autoParam
  (Function.RightInverse
    (fun (a : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
      And.casesOn (motive := fun (x : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        (X ≅ 0) × (Y ≅ 0)) a fun (hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0) (hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0) ↦
        ((idZeroEquivIsoZero X : (a : 𝟙 X = 0) → X ≅ 0) hX, (idZeroEquivIsoZero Y : (a : 𝟙 Y = 0) → Y ≅ 0) hY))
    sorry)
  Equiv.right_inv._autoParam
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have toFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
toFun : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0 ∧ Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
have toFun₁ : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
⊢ (X ≅ 0) × (Y ≅ 0)
have invFun : X ≅ 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
X Y : C
hX : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
hY : Eq.{v + 1} (α := Y ⟶ Y) (𝟙 Y) 0
invFun : X ≅ 0
⊢ (X ≅ 0) × (Y ≅ 0)
have invFun₁ : Y ≅ 0
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 ↔ IsZero.{v, u} X ∧ IsZero.{v, u} Y
have mp : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 → IsZero.{v, u} X ∧ IsZero.{v, u} Y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
mp : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 → IsZero.{v, u} X ∧ IsZero.{v, u} Y
⊢ IsIso.{v, u} (C := C) (X := X) (Y := Y) 0 ↔ IsZero.{v, u} X ∧ IsZero.{v, u} Y
have mpr : IsZero.{v, u} X ∧ IsZero.{v, u} Y → IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso f
have rw : IsIso.{v, u} (C := C) (X := X) (Y := Y) 0
Tactic: rw [zero_of_source_iso_zero f i]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
⊢ HasZeroObject.{v, u} C
have refine : ∀ (X : C) (f : X ⟶ initial.{v, u} C), f = default
Tactic: refine ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
⊢ f ≫ 𝟙 (initial.{v, u} C) = f ≫ 0
have h : Eq.{v + 1} (α := initial.{v, u} C ⟶ initial.{v, u} C) (𝟙 (initial.{v, u} C)) 0
Tactic: congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
f : X ⟶ initial.{v, u} C
⊢ f = default
have f₁ : f ≫ 𝟙 (initial.{v, u} C) = f ≫ 0
Tactic: calc
    f = f ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = f ≫ 0 := by congr!; subsingleton
    _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
⊢ HasZeroObject.{v, u} C
have refine : ∀ (X : C) (f : terminal.{v, u} C ⟶ X), f = default
Tactic: refine ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
⊢ 𝟙 (terminal.{v, u} C) ≫ f = 0 ≫ f
have h : Eq.{v + 1} (α := terminal.{v, u} C ⟶ terminal.{v, u} C) (𝟙 (terminal.{v, u} C)) 0
Tactic: congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasTerminal.{v, u} C
X : C
f : terminal.{v, u} C ⟶ X
⊢ f = default
have f₁ : 𝟙 (terminal.{v, u} C) ≫ f = 0 ≫ f
Tactic: calc
    f = 𝟙 _ ≫ f := (Category.id_comp _).symm
    _ = 0 ≫ f := by congr!; subsingleton
    _ = 0 := zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X Y : C
inst_3 : HasImage.{v, u} (C := C) (X := X) (Y := Y) 0
⊢ Eq.{v + 1} (α := image.{v, u} (X := X) (Y := Y) 0 ⟶ Y) (ι 0) 0
have rw : Eq.{v + 1} (α := image.{v, u} (X := X) (Y := Y) 0 ⟶ Y)
  (CategoryStruct.comp (Y := MonoFactorisation.I.{v, u} (f := 0) (monoFactorisationZero X Y))
    (lift (monoFactorisationZero X Y)) (MonoFactorisation.m (monoFactorisationZero X Y)))
  0
Tactic: rw [← image.lift_fac (monoFactorisationZero X Y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasEqualizers.{v, u} C
X Y : C
f : X ⟶ Y
h : f = 0
inst_4 : HasImage f
⊢ Eq (α := image f ⟶ Y) (ι f) 0
have rw : Eq (α := image f ⟶ Y) (CategoryStruct.comp (Y := image.{v, u} (X := X) (Y := Y) 0) (Iso.hom (eqToIso h)) (ι 0)) 0
Tactic: rw [image.eq_fac h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
X Y : D
f : X ⟶ Y
x : D
⊢ Eq (α := X ⟶ x) (f ≫ 0) 0
have apply : Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ 0)) (F.map 0)
Tactic: apply hF.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
X Y : D
f : X ⟶ Y
x : D
⊢ Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ 0)) (F.map 0)
have change : Eq (α := F.obj X ⟶ F.obj x) (F.map (f ≫ hF.preimage 0)) (F.map (hF.preimage 0))
Tactic: change F.map (f ≫ (hF.preimage _)) = F.map (hF.preimage _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
F : Functor.{v', v, u', u} D C
hF : F.FullyFaithful
x x_1 x_2 : D
f : x_1 ⟶ x_2
⊢ Eq (α := x ⟶ x_2) (0 ≫ f) 0
have apply : Eq (α := F.obj x ⟶ F.obj x_2) (F.map (0 ≫ f)) (F.map 0)
Tactic: apply hF.map_injective