awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
rw : (S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯) ≫ S.f = 𝟙 S.X₁ ≫ S.f
rw₁ : S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ ≫ S.f = 𝟙 S.X₁ ≫ S.f
rw₂ : S.f ≫ (𝟙 S.X₂ - S.g ≫ s) = 𝟙 S.X₁ ≫ S.f
rw₃ : S.f ≫ 𝟙 S.X₂ - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
rw₄ : S.f - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
rw₅ : S.f - 0 ≫ s = 𝟙 S.X₁ ≫ S.f
rw₆ : S.f - 0 = 𝟙 S.X₁ ≫ S.f
rw₇ : S.f = 𝟙 S.X₁ ≫ S.f
⊢ S.f ≫ hS.lift (𝟙 S.X₂ - S.g ≫ s) ⋯ = 𝟙 S.X₁
have rw₈ : S.f = S.f
Tactic: rw [← cancel_mono S.f, assoc, Exact.lift_f, comp_sub, comp_id,
    zero_assoc, zero_comp, sub_zero, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) sorry ≫ S.g = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₄ : S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₄ : S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₅ : S.g - r ≫ 0 = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₄ : S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₅ : S.g - r ≫ 0 = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₆ : S.g - 0 = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₄ : S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₅ : S.g - r ≫ 0 = S.g ≫ 𝟙 S.X₃
rw₆ : S.g - 0 = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₇ : S.g = S.g ≫ 𝟙 S.X₃
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
r : S.X₂ ⟶ S.X₁
f_r : S.f ≫ r = 𝟙 S.X₁
hg : Epi S.g
rw : S.g ≫ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₁ : (𝟙 S.X₂ - r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₂ : 𝟙 S.X₂ ≫ S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₃ : S.g - (r ≫ S.f) ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₄ : S.g - r ≫ S.f ≫ S.g = S.g ≫ 𝟙 S.X₃
rw₅ : S.g - r ≫ 0 = S.g ≫ 𝟙 S.X₃
rw₆ : S.g - 0 = S.g ≫ 𝟙 S.X₃
rw₇ : S.g = S.g ≫ 𝟙 S.X₃
⊢ hS.desc (𝟙 S.X₂ - r ≫ S.f) ⋯ ≫ S.g = 𝟙 S.X₃
have rw₈ : S.g = S.g
Tactic: rw [← cancel_epi S.g, Exact.g_desc_assoc, sub_comp, id_comp, assoc, zero,
      comp_zero, sub_zero, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
⊢ PreservesFiniteLimits F
have this : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
Tactic: have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesKernel F f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesFiniteLimits F
have this₁ : HasBinaryBiproducts.{v_1, u_1} C
Tactic: have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this : HasBinaryBiproducts.{v_1, u_1} C
⊢ PreservesFiniteLimits F
have this₁ : HasEqualizers.{v_1, u_1} C
Tactic: have : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₃ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteProducts.{v_1, u_1} C
inst_8 : HasKernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasEqualizers.{v_1, u_1} C
⊢ PreservesFiniteLimits F
have this₁ : HasZeroObject.{v_2, u_2} D
Tactic: have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
⊢ PreservesFiniteColimits F
have this : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
Tactic: have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesCokernel F f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
⊢ PreservesFiniteColimits F
have this₁ : HasBinaryBiproducts.{v_1, u_1} C
Tactic: have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryCoproducts
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this : HasBinaryBiproducts.{v_1, u_1} C
⊢ PreservesFiniteColimits F
have this₁ : HasCoequalizers.{v_1, u_1} C
Tactic: have : HasCoequalizers C := Preadditive.hasCoequalizers_of_hasCokernels
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
rw : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map (𝟙 0)) 0
rw₂ : Eq (α := F.obj 0 ⟶ F.obj 0) (F.map 0) 0
⊢ IsZero.{v_2, u_2} (F.obj 0)
have rw₃ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
inst_5 : F.PreservesHomology
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasFiniteCoproducts.{v_1, u_1} C
inst_8 : HasCokernels.{v_1, u_1} C
this_1 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_2 : HasBinaryBiproducts.{v_1, u_1} C
this : HasCoequalizers.{v_1, u_1} C
⊢ PreservesFiniteColimits F
have this₁ : HasZeroObject.{v_2, u_2} D
Tactic: have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
⊢ Exact (S.map F) ∧ Mono (F.map S.f)
have this : F.PreservesMonomorphisms
Tactic: have := preservesMonomorphisms_of_preserves_shortExact_left F hF
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
⊢ Exact (S.map F) ∧ Mono (F.map S.f)
have refine : Exact (S.map F)
Tactic: refine ⟨?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
⊢ 𝟙 (F.obj T.X₂) ≫ F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
have rw : F.map S.g =
  CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
    (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
Tactic: rw [Category.id_comp, ← F.map_comp, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
rw :
  F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
⊢ 𝟙 (F.obj T.X₂) ≫ F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
have rw₁ : F.map S.g =
  F.map
    (CategoryStruct.comp (Y := cokernel (X := Limits.kernel S.g) (kernel.ι S.g)) (cokernel.π (kernel.ι S.g))
      (Abelian.factorThruCoimage S.g))
Tactic: rw [Category.id_comp, ← F.map_comp, cokernel.π_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ExactFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Mono (F.map S.f)
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex.{v_1, u_1} C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
rw :
  F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
rw₁ :
  F.map S.g =
    F.map
      (CategoryStruct.comp (Y := cokernel (X := Limits.kernel S.g) (kernel.ι S.g)) (cokernel.π (kernel.ι S.g))
        (Abelian.factorThruCoimage S.g))
⊢ 𝟙 (F.obj T.X₂) ≫ F.map S.g =
    CategoryStruct.comp (Y := F.obj (cokernel (X := Limits.kernel S.g) (kernel.ι S.g)))
      (F.map (cokernel.π (kernel.ι S.g))) (F.map (Abelian.factorThruCoimage S.g))
have rw₂ : F.map S.g = F.map S.g
Tactic: rw [Category.id_comp, ← F.map_comp, cokernel.π_desc]