-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma homologySequence_exact₁ :
    (ShortComplex.mk _ _ (F.homologySequenceδ_comp T hT _ _ h)).Exact

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (-(F.shiftIso (-1) n₁ n₀ ⋯).hom.app T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h =
    (F.shift n₁).map (-(shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁) ≫
      𝟙 ((F.shift n₁).obj T.obj₁)

Tactic:
simp only [homologySequenceδ, neg_comp, map_neg, comp_id,
  F.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero T.mor₃ (-1) (neg_add_cancel 1) n₀ n₁ (by omega)]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (inv_rot_of_distTriang _ hT) n₁)

Result:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯ ≅
    ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯ ≅
    ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯

Tactic:
refine ShortComplex.isoMk (-((F.shiftIso (-1) n₁ n₀ (by omega)).app _))
  (Iso.refl _) (Iso.refl _) ?_ (by simp)

Result:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (-(F.shiftIso (-1) n₁ n₀ ⋯).app T.obj₃).hom ≫
      (ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).f =
    (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).f ≫
      (Iso.refl (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).X₂).hom

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (-(F.shiftIso (-1) n₁ n₀ ⋯).app T.obj₃).hom ≫
      (ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).f =
    (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).f ≫
      (Iso.refl (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).X₂).hom

Tactic:
dsimp

Result:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (-(F.shiftIso (-1) n₁ n₀ ⋯).hom.app T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h =
    (F.shift n₁).map (-(shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁) ≫
      𝟙 ((F.shift n₁).obj T.obj₁)

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (Iso.refl (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).X₂).hom ≫
      (ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).g =
    (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).g ≫
      (Iso.refl (ShortComplex.mk ((F.shift n₁).map T.invRotate.mor₁) ((F.shift n₁).map T.invRotate.mor₂) ⋯).X₃).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_5, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_4, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ -1 + n₁ = n₀

Tactic:
omega

Result:
no goals