awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : F.PreservesZeroMorphisms
⊢ F.IsHomological
have this₁ : (L ⋙ F).IsHomological
Tactic: have : (L ⋙ F).IsHomological := IsHomological.of_iso e.symm
-- 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
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
have 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' sorry).map F)
Tactic: refine IsHomological.mk' _ (fun T hT => ?_)
-- 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
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_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
have hT₁ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
Tactic: rw [L.distTriang_iff] at 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
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
⊢ ∃ (T' : Triangle.{v_2, u_2} D) (e : T ≅ T'), ShortComplex.Exact ((shortComplexOfDistTriangle T' ⋯).map F)
have 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' sorry).map F)
Tactic: obtain ⟨T₀, e, hT₀⟩ := hT
Cleared hypotheses: 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 : F.ShiftSequence ℤ
T : Triangle.{v_1, u_1} C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁
have rw₁ : n₁ = n₁
Tactic: rw [add_comm 1, h]
-- 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 : F.ShiftSequence ℤ
T T' : Triangle.{v_1, u_1} C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.homologySequenceδ T' n₀ n₁ h = F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map φ.hom₁
have dsimp : (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ sorry = F.shiftMap T.mor₃ n₀ n₁ sorry ≫ (F.shift n₁).map φ.hom₁
Tactic: dsimp only [homologySequenceδ]
-- 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 : F.ShiftSequence ℤ
T T' : Triangle.{v_1, u_1} C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
have rw : F.shiftMap (φ.hom₃ ≫ T'.mor₃) n₀ n₁ sorry = F.shiftMap T.mor₃ n₀ n₁ sorry ≫ (F.shift n₁).map φ.hom₁
Tactic: rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]
-- 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 : 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₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
have rw₁ : F.shiftMap (T.mor₃ ≫ map (shiftFunctor C (A := ℤ) 1) φ.hom₁) n₀ n₁ sorry =
  F.shiftMap T.mor₃ n₀ n₁ sorry ≫ (F.shift n₁).map φ.hom₁
Tactic: rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]
-- 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 : 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₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁
have rw₂ : F.shiftMap T.mor₃ n₀ n₁ sorry ≫ (F.shift n₁).map φ.hom₁ = F.shiftMap T.mor₃ n₀ n₁ sorry ≫ (F.shift n₁).map φ.hom₁
Tactic: rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]
-- 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.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₁
⊢ (F.shift n₀).map T.mor₂ ≫ F.homologySequenceδ T n₀ n₁ h = 0
have dsimp : (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ sorry = 0
Tactic: dsimp only [homologySequenceδ]
-- 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.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₁
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0
have rw : Eq (α := (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₁).obj T.obj₁) (F.shiftMap (T.mor₂ ≫ T.mor₃) n₀ n₁ sorry) 0
Tactic: rw [← F.shiftMap_comp', comp_distTriang_mor_zero₂₃ _ hT, shiftMap_zero]
-- 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.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
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0
have rw₁ : Eq (α := (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₁).obj T.obj₁) (F.shiftMap 0 n₀ n₁ sorry) 0
Tactic: rw [← F.shiftMap_comp', comp_distTriang_mor_zero₂₃ _ hT, shiftMap_zero]
-- 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.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
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0
have rw₂ : Eq.{v_3 + 1} (α := (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₁).obj T.obj₁) 0 0
Tactic: rw [← F.shiftMap_comp', comp_distTriang_mor_zero₂₃ _ hT, shiftMap_zero]
-- 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.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₁
⊢ F.homologySequenceδ T n₀ n₁ h ≫ (F.shift n₁).map T.mor₁ = 0
have dsimp : F.shiftMap T.mor₃ n₀ n₁ sorry ≫ (F.shift n₁).map T.mor₁ = 0
Tactic: dsimp only [homologySequenceδ]
-- 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.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₁
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0
have 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₁ sorry) 0
Tactic: rw [← F.shiftMap_comp, comp_distTriang_mor_zero₃₁ _ hT, shiftMap_zero]
-- 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.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
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0
have rw₁ : Eq (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₂) (F.shiftMap 0 n₀ n₁ sorry) 0
Tactic: rw [← F.shiftMap_comp, comp_distTriang_mor_zero₃₁ _ hT, shiftMap_zero]
-- 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.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
⊢ F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map T.mor₁ = 0
have rw₂ : Eq.{v_3 + 1} (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₂) 0 0
Tactic: rw [← F.shiftMap_comp, comp_distTriang_mor_zero₃₁ _ hT, shiftMap_zero]
-- 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.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₀ : ℤ
⊢ (F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0
have rw : (F.shift n₀).map (T.mor₁ ≫ T.mor₂) = 0
Tactic: rw [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero]
-- 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.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
⊢ (F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0
have rw₁ : Eq (α := (F.shift n₀).obj T.obj₁ ⟶ (F.shift n₀).obj T.obj₃) ((F.shift n₀).map 0) 0
Tactic: rw [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero]
-- 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.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
⊢ (F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0
have rw₂ : Eq.{v_3 + 1} (α := (F.shift n₀).obj T.obj₁ ⟶ (F.shift n₀).obj T.obj₃) 0 0
Tactic: rw [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT, Functor.map_zero]
-- 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.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 := ⋯ }
have refine : Iso (C := ShortComplex.{v_3, u_3} A)
  ((shortComplexOfDistTriangle (obj (shiftFunctor (Triangle.{v_1, u_1} C) n₀) T) sorry).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 := sorry }
Tactic: refine ShortComplex.exact_of_iso ?_ (F.map_distinguished_exact _
    (Triangle.shift_distinguished _ hT n₀))
-- 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.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₁
⊢ 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.homologySequenceδ T n₀ n₁ h, zero := ⋯ }
have refine : Iso (C := ShortComplex.{v_3, u_3} A)
  { X₁ := (F.shift n₀).obj T.rotate.obj₁, X₂ := (F.shift n₀).obj T.rotate.obj₂, X₃ := (F.shift n₀).obj T.rotate.obj₃,
    f := (F.shift n₀).map T.rotate.mor₁, g := (F.shift n₀).map T.rotate.mor₂, zero := sorry }
  { 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.homologySequenceδ T n₀ n₁ h, zero := sorry }
Tactic: refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (rot_of_distTriang _ hT) n₀)
-- 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.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₁
⊢ 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.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ }
have refine : Iso (C := ShortComplex.{v_3, u_3} A)
  { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
    X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
    g := (F.shift n₁).map T.invRotate.mor₂, zero := sorry }
  { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
    f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := sorry }
Tactic: refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (inv_rot_of_distTriang _ hT) n₁)