awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 :
  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₂)
this : PreservesBinaryBiproduct X₁ X₂ F
⊢ PreservesLimit (pair X₁ X₂) F

Tactic:
apply Limits.preservesBinaryProduct_of_preservesBinaryBiproduct

Premises used: CategoryTheory.Limits.preservesBinaryProduct_of_preservesBinaryBiproduct
-- 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
⊢ F.Additive

Tactic:
F.additive_of_preserves_binary_products

Premises used: CategoryTheory.Functor.additive_of_preserves_binary_products
-- 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
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.PreservesZeroMorphisms

Tactic:
have : F.PreservesZeroMorphisms := preservesZeroMorphisms_of_map_zero_object
    (F.mapIso L.mapZeroObject.symm ≪≫ e.app _ ≪≫ G.mapZeroObject)
-- 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
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
this : F.PreservesZeroMorphisms
⊢ (L ⋙ F).IsHomological

Tactic:
have : (L ⋙ F).IsHomological := IsHomological.of_iso e.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
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
this_1 : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
⊢ F.IsHomological

Tactic:
IsHomological.mk' _ (fun T hT => ?_)

Premises used: 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
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
this_1 : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
refine :
  ∀ (T : Triangle.{v_2, u_2} D)
    (hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_6 _) T),
    ∃ (T' : Triangle.{v_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
⊢ F.IsHomological

Tactic:
refine IsHomological.mk' _ (fun T hT => ?_)

Premises used: 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
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
this_1 : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_6 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
rw [L.distTriang_iff] at hT

Premises used: CategoryTheory.Functor.distTriang_iff
-- 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
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
this_1 : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
T : Triangle.{v_2, u_2} D
hT_1 : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_6 _) T
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
obtain :
  ∀ (T₀ : Triangle.{v_1, u_1} C) (e : T ≅ obj L.mapTriangle T₀)
    (hT₀ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T₀),
    ∃ (T' : Triangle.{v_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
⊢ ∃ (T' : Triangle.{v_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)

Tactic:
obtain ⟨T₀, e, hT₀⟩ := hT
-- 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
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_1 : L ⋙ F ≅ G
inst_17 : G.IsHomological
this_1 : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_6 _) T
T₀ : Triangle.{v_1, u_1} C
e : T ≅ obj L.mapTriangle T₀
hT₀ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T₀
⊢ ∃ (T' : Triangle.{v_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)

Tactic:
⟨L.mapTriangle.obj T₀, e, (L ⋙ F).map_distinguished_exact _ hT₀⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.mapTriangle, CategoryTheory.Functor.map_distinguished_exact, Exists.intro, CategoryTheory.Functor.obj
-- 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
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_1 : L ⋙ F ≅ G
inst_17 : G.IsHomological
this_1 : F.PreservesZeroMorphisms
this : (L ⋙ F).IsHomological
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_6 _) T
T₀ : Triangle.{v_1, u_1} C
e : T ≅ obj L.mapTriangle T₀
hT₀ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T₀
⊢ ∃ (T' : Triangle.{v_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)

Tactic:
exact ⟨L.mapTriangle.obj T₀, e, (L ⋙ F).map_distinguished_exact _ hT₀⟩
-- 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 : F.ShiftSequence ℤ
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw : n₀ + 1 = n₁
rw₁ rw₂ : n₁ = n₁
⊢ 1 + n₀ = n₁

Tactic:
rw [add_comm 1, h]

Premises used: add_comm, OfNat.ofNat
-- 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 : F.ShiftSequence ℤ
T T' : Triangle.{v_1, u_1} C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
dsimp : (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.homologySequenceδ T' n₀ n₁ h = F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map φ.hom₁

Tactic:
dsimp only [homologySequenceδ]

Premises used: CategoryTheory.Functor.homologySequenceδ
-- 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 : F.ShiftSequence ℤ
T T' : Triangle.{v_1, u_1} C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw : F.shiftMap (φ.hom₃ ≫ T'.mor₃) n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
rw₁ :
  F.shiftMap (T.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) φ.hom₁) n₀ n₁ ⋯ =
    F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
rw₂ rw₃ : F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁

Tactic:
rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]

Premises used: CategoryTheory.Functor.shiftMap_comp', CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CategoryTheory.Functor.shiftMap_comp
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
dsimp : (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0
⊢ (F.shift n₀).map T.mor₂ ≫ F.homologySequenceδ T n₀ n₁ h = 0

Tactic:
dsimp only [homologySequenceδ]

Premises used: CategoryTheory.Functor.homologySequenceδ
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw : Eq (α := (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₁).obj T.obj₁) (F.shiftMap (T.mor₂ ≫ T.mor₃) n₀ n₁ ⋯) 0
rw₁ : Eq (α := (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₁).obj T.obj₁) (F.shiftMap 0 n₀ n₁ ⋯) 0
rw₂ rw₃ : Eq.{v_3 + 1} (α := (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₁).obj T.obj₁) 0 0
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0

Tactic:
rw [← F.shiftMap_comp', comp_distTriang_mor_zero₂₃ _ hT, shiftMap_zero]

Premises used: CategoryTheory.Functor.shiftMap_comp', CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CategoryTheory.Functor.shiftMap_zero
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
dsimp : F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0
⊢ F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map T.mor₁ = 0

Tactic:
dsimp only [homologySequenceδ]

Premises used: CategoryTheory.Functor.homologySequenceδ
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw :
  Eq (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₂)
    (F.shiftMap (T.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) T.mor₁) n₀ n₁ ⋯) 0
rw₁ : Eq (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₂) (F.shiftMap 0 n₀ n₁ ⋯) 0
rw₂ rw₃ : Eq.{v_3 + 1} (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₂) 0 0
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0

Tactic:
rw [← F.shiftMap_comp, comp_distTriang_mor_zero₃₁ _ hT, shiftMap_zero]

Premises used: CategoryTheory.Functor.shiftMap_comp, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, CategoryTheory.Functor.shiftMap_zero
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ : ℤ
rw : (F.shift n₀).map (T.mor₁ ≫ T.mor₂) = 0
rw₁ : Eq (α := (F.shift n₀).obj T.obj₁ ⟶ (F.shift n₀).obj T.obj₃) ((F.shift n₀).map 0) 0
rw₂ rw₃ : Eq.{v_3 + 1} (α := (F.shift n₀).obj T.obj₁ ⟶ (F.shift n₀).obj T.obj₃) 0 0
⊢ (F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0

Tactic:
rw [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero]

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ : ℤ
⊢ ShortComplex.Exact
    { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
      f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }

Tactic:
ShortComplex.exact_of_iso ?_ (F.map_distinguished_exact _
    (Triangle.shift_distinguished _ hT n₀))

Premises used: CategoryTheory.Pretriangulated.Triangle.shift_distinguished, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Functor.map_distinguished_exact
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ : ℤ
refine :
  Iso (C := ShortComplex.{v_3, u_3} A)
    ((shortComplexOfDistTriangle (obj (shiftFunctor (Triangle.{v_1, u_1} C) n₀) T) ⋯).map F)
    { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
      f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }
⊢ ShortComplex.Exact
    { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
      f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.map_distinguished_exact _
    (Triangle.shift_distinguished _ hT n₀))

Premises used: CategoryTheory.Pretriangulated.Triangle.shift_distinguished, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Functor.map_distinguished_exact
-- 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.IsHomological
inst_9 : F.ShiftSequence ℤ
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
n₀ : ℤ
⊢ CategoryStruct.comp (Y :=
      ShortComplex.X₁
        { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
          f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ })
      (Iso.hom (Iso.app (F.isoShift n₀) T.obj₁))
      (ShortComplex.f
        { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
          f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }) =
    ShortComplex.f ((shortComplexOfDistTriangle (obj (shiftFunctor (Triangle.{v_1, u_1} C) n₀) T) ⋯).map F) ≫
      (HSMul.hSMul (β := (shiftFunctor C n₀ ⋙ F).obj T.obj₂ ≅ (F.shift n₀).obj T.obj₂) n₀.negOnePow
          (Iso.app (F.isoShift n₀) T.obj₂)).hom

Tactic:
simp