awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
⊢ P.triangEnvelope ≤ Q
have rw : ∀ (i : ℕ), P.triangEnvelopeIter i ≤ Q
Tactic: rw [triangEnvelope, iSup_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ P.triangEnvelopeIter n ≤ Q
have rw : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q
Tactic: rw [triangEnvelopeIter, retractClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤ Q
have h₁ : (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ Q
Tactic: apply extensionProductIter_le_of_isTriangulatedClosed₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ Q
have h₁ : (P.shiftClosure ℤ).binaryProductsClosure ≤ Q
Tactic: rwa [retractClosure_le_iff, binaryProductsClosure_le_iff, shiftClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsStableUnderRetracts
inst_7 : Q.IsTriangulated
h : P ≤ Q
n : ℕ
h₁ : (P.shiftClosure ℤ).binaryProductsClosure ≤ Q
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure ≤ Q
have h₂ : P.shiftClosure ℤ ≤ Q
Tactic: rwa [retractClosure_le_iff, binaryProductsClosure_le_iff, shiftClosure_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
h : P.IsStrongTriangulatedGenerator
⊢ P.IsClassicalTriangulatedGenerator
have obtain : ∀ (n : ℕ) (hn : P.triangEnvelopeIter n = ⊤), P.IsClassicalTriangulatedGenerator
Tactic: obtain ⟨n, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Generators (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
n : ℕ
hn : P.triangEnvelopeIter n = ⊤
⊢ P.IsClassicalTriangulatedGenerator
have rw : ⊤ ≤ P.triangEnvelope
Tactic: rw [isClassicalTriangulatedGenerator_iff, eq_top_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.PreservesZeroMorphisms
hF :
  ∀ (T : Triangle.{v_1, u_1} C)
    (hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _) T),
    ∃ (T' : Triangle.{v_1, u_1} C) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _) T
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)
have obtain : ∀ (T' : Triangle.{v_1, u_1} C) (e : T ≅ T') (h' : ShortComplex.Exact ((shortComplexOfDistTriangle T' sorry).map F)),
  ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)
Tactic: obtain ⟨T', e, h'⟩ := hF T hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F
have suffices : ∀ (X₁ X₂ : C), PreservesLimit (pair X₁ X₂) F
Tactic: suffices ∀ (X₁ X₂ : C), PreservesLimit (pair X₁ X₂) F from
    ⟨fun {X} => preservesLimit_of_iso_diagram F (diagramIsoPair X).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
⊢ PreservesLimit (pair X₁ X₂) F
have this : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Tactic: have : HasBinaryBiproduct (F.obj X₁) (F.obj X₂) := HasBinaryBiproducts.has_binary_biproduct _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
⊢ Mono (X := F.obj (biprod.{v_1, u_1} X₁ X₂)) (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (F.biprodComparison X₁ X₂)
have rw : ∀ (P : A) (g : P ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)),
  Eq (α := P ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (g ≫ F.biprodComparison X₁ X₂) 0 → g = 0
Tactic: rw [mono_iff_cancel_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
f : Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)
hf : Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (f ≫ F.biprodComparison X₁ X₂) 0
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
⊢ Mono S.f
have dsimp : Mono (X := F.obj X₁) (Y := F.obj (biprod.{v_1, u_1} X₁ X₂)) (F.map biprod.inl)
Tactic: dsimp [S]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
f : Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)
hf : Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (f ≫ F.biprodComparison X₁ X₂) 0
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
⊢ f = 0
have this₁ : Mono S.f
Tactic: have : Mono S.f := by dsimp [S]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
f : Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)
hf : Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (f ≫ F.biprodComparison X₁ X₂) 0
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
⊢ f = 0
have ex : S.Exact
Tactic: have ex : S.Exact := F.map_distinguished_exact _ (binaryBiproductTriangle_distinguished X₁ X₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
f : Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)
hf : Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (f ≫ F.biprodComparison X₁ X₂) 0
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
ex : S.Exact
⊢ f = 0
have obtain : ∀ (g : Z ⟶ S.X₁) (hf : Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) ((g ≫ S.f) ≫ F.biprodComparison X₁ X₂) 0),
  g ≫ S.f = 0
Tactic: obtain ⟨g, rfl⟩ := ex.lift' f (by simpa using hf =≫ biprod.snd)
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf : Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) ((g ≫ S.f) ≫ F.biprodComparison X₁ X₂) 0
⊢ g ≫ S.f = 0
have dsimp : Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0
Tactic: dsimp [S] at hf ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf :
  Eq (α := Z ⟶ biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂))
    (CategoryStruct.comp (Y := F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) (F.biprodComparison X₁ X₂)) 0
⊢ Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0
have hf₁ : CategoryStruct.comp (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂))
    (CategoryStruct.comp (Y := F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) (F.biprodComparison X₁ X₂))
    biprod.fst =
  CategoryStruct.comp (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) 0 biprod.fst
Tactic: replace hf := hf =≫ biprod.fst
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf :
  CategoryStruct.comp (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂))
      (CategoryStruct.comp (Y := F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) (F.biprodComparison X₁ X₂))
      biprod.fst =
    CategoryStruct.comp (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) 0 biprod.fst
⊢ Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0
have hf₁ : g = 0
Tactic: simp only [assoc, biprodComparison_fst, zero_comp, ← F.map_comp, biprod.inl_fst,
      F.map_id, comp_id] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf : g = 0
⊢ Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0
have rw : Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (0 ≫ F.map biprod.inl) 0
Tactic: rw [hf, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
Z : A
S : ShortComplex.{v_3, u_3} A :=
  ShortComplex.map (ShortComplex.mk (X₁ := X₁) (X₂ := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd ⋯) F
this : Mono S.f
ex : S.Exact
g : Z ⟶ S.X₁
hf : g = 0
rw : Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (0 ≫ F.map biprod.inl) 0
⊢ Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0
have rw₁ : Eq.{v_3 + 1} (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) 0 0
Tactic: rw [hf, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
⊢ PreservesLimit (pair X₁ X₂) F
have this₁ : Mono (X := F.obj (biprod.{v_1, u_1} X₁ X₂)) (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (F.biprodComparison X₁ X₂)
Tactic: have : Mono (F.biprodComparison X₁ X₂) := by
    rw [mono_iff_cancel_zero]
    intro Z f hf
    let S := (ShortComplex.mk _ _ (biprod.inl_snd (X := X₁) (Y := X₂))).map F
    have : Mono S.f := by dsimp [S]; infer_instance
    have ex : S.Exact := F.map_distinguished_exact _ (binaryBiproductTriangle_distinguished X₁ X₂)
    obtain ⟨g, rfl⟩ := ex.lift' f (by simpa using hf =≫ biprod.snd)
    dsimp [S] at hf ⊢
    replace hf := hf =≫ biprod.fst
    simp only [assoc, biprodComparison_fst, zero_comp, ← F.map_comp, biprod.inl_fst,
      F.map_id, comp_id] at hf
    rw [hf, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
inst_14 : F.IsHomological
X₁ X₂ : C
this_1 : HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)
this :
  Mono (X := F.obj (biprod.{v_1, u_1} X₁ X₂)) (Y := biprod.{v_3, u_3} (F.obj X₁) (F.obj X₂)) (F.biprodComparison X₁ X₂)
⊢ PreservesLimit (pair X₁ X₂) F
have this₁ : PreservesBinaryBiproduct X₁ X₂ F
Tactic: have : PreservesBinaryBiproduct X₁ X₂ F := preservesBinaryBiproduct_of_mono_biprodComparison _
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_7 : Pretriangulated.{v_2, u_2} D
inst_8 : Category.{v_3, u_3} A
inst_9 : HasZeroObject.{v_1, u_1} C
inst_10 : Preadditive.{v_1, u_1} C
inst_11 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_12 : Pretriangulated.{v_1, u_1} C
inst_13 : Abelian.{v_3, u_3} A
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_14 : L.CommShift ℤ
inst_15 : L.IsTriangulated
inst_16 : L.mapArrow.EssSurj
F : Functor.{v_2, v_3, u_2, u_3} D A
G : Functor.{v_1, v_3, u_1, u_3} C A
e : L ⋙ F ≅ G
inst_17 : G.IsHomological
⊢ F.IsHomological
have this : F.PreservesZeroMorphisms
Tactic: have : F.PreservesZeroMorphisms := preservesZeroMorphisms_of_map_zero_object
    (F.mapIso L.mapZeroObject.symm ≪≫ e.app _ ≪≫ G.mapZeroObject)