awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
obtain :
  ∀ (T' : Triangle.{v_1, u_1} C) (e : T ≅ T') (h' : ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)),
    ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)

Tactic:
obtain ⟨T', e, h'⟩ := hF T hT
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
T' : Triangle.{v_1, u_1} C
e : T ≅ T'
h' : ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)

Tactic:
(ShortComplex.exact_iff_of_iso
      (F.mapShortComplex.mapIso ((shortComplexOfDistTriangleIsoOfIso e hT)))).2 h'

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso, CategoryTheory.ShortComplex.exact_iff_of_iso, CategoryTheory.Functor.mapShortComplex, CategoryTheory.ShortComplex.map, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
T' : Triangle.{v_1, u_1} C
e : T ≅ T'
h' : ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
⊢ ShortComplex.Exact ((shortComplexOfDistTriangle T hT).map F)

Tactic:
exact (ShortComplex.exact_iff_of_iso
      (F.mapShortComplex.mapIso ((shortComplexOfDistTriangleIsoOfIso e hT)))).2 h'

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso, CategoryTheory.ShortComplex.exact_iff_of_iso, CategoryTheory.Functor.mapShortComplex, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
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
F₁ F₂ : Functor.{v_1, v_3, u_1, u_3} C A
inst_8 : F₁.IsHomological
e : F₁ ≅ F₂
⊢ F₂.IsHomological

Tactic:
have := preservesZeroMorphisms_of_iso e
  ⟨fun T hT => ShortComplex.exact_of_iso (ShortComplex.mapNatIso _ e)
    (F₁.map_distinguished_exact T hT)⟩

Premises used: CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Functor.preservesZeroMorphisms_of_iso, CategoryTheory.Functor.map_distinguished_exact, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle, CategoryTheory.ShortComplex.mapNatIso, CategoryTheory.Functor.IsHomological.mk
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
suffices : ∀ (X₁ X₂ : C), PreservesLimit (pair X₁ X₂) F
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
suffices ∀ (X₁ X₂ : C), PreservesLimit (pair X₁ X₂) F from
    ⟨fun {X} => preservesLimit_of_iso_diagram F (diagramIsoPair X).symm⟩
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
⊢ HasBinaryBiproduct.{v_3, u_3} (F.obj X₁) (F.obj X₂)

Tactic:
have : HasBinaryBiproduct (F.obj X₁) (F.obj X₂) := HasBinaryBiproducts.has_binary_biproduct _ _
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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₂)
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
⊢ 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:
rw [mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_zero
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
dsimp : Mono (X := F.obj X₁) (Y := F.obj (biprod.{v_1, u_1} X₁ X₂)) (F.map biprod.inl)
⊢ Mono S.f

Tactic:
dsimp [S]
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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 (X := F.obj X₁) (Y := F.obj (biprod.{v_1, u_1} X₁ X₂)) (F.map biprod.inl)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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

Tactic:
have : Mono S.f := by dsimp [S]; infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
⊢ S.Exact

Tactic:
have ex : S.Exact := F.map_distinguished_exact _ (binaryBiproductTriangle_distinguished X₁ X₂)
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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 ≫ S.g = 0

Tactic:
simpa using hf =≫ biprod.snd

Premises used: CategoryTheory.Limits.biprod.snd
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
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
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := ex.lift' f (by simpa using hf =≫ biprod.snd)

Premises used: CategoryTheory.ShortComplex.Exact.lift', rfl
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
dsimp : Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0
⊢ g ≫ S.f = 0

Tactic:
dsimp [S] at hf ⊢
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
⊢ g = 0

Tactic:
simp only [assoc, biprodComparison_fst, zero_comp, ← F.map_comp, biprod.inl_fst,
      F.map_id, comp_id] at hf

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.biprodComparison_fst, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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
rw₁ rw₂ : Eq.{v_3 + 1} (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) 0 0
⊢ Eq (α := Z ⟶ F.obj (biprod.{v_1, u_1} X₁ X₂)) (g ≫ F.map biprod.inl) 0

Tactic:
rw [hf, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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₂)

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]
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
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₂)
⊢ PreservesBinaryBiproduct X₁ X₂ F

Tactic:
have : PreservesBinaryBiproduct X₁ X₂ F := preservesBinaryBiproduct_of_mono_biprodComparison _