-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma homologySequence_exact₃ :
    (ShortComplex.mk _ _ (F.comp_homologySequenceδ 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₁
⊢ (Iso.refl (ShortComplex.mk ((F.shift n₀).map T.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯).X₁).hom ≫
      (ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯).f =
    (ShortComplex.mk ((F.shift n₀).map T.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯).f ≫
      (Iso.refl (ShortComplex.mk ((F.shift n₀).map T.rotate.mor₁) ((F.shift n₀).map T.rotate.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₁
⊢ (ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯).Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (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.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯ ≅
    ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯

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.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯).X₂).hom ≫
      (ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯).g =
    (ShortComplex.mk ((F.shift n₀).map T.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯).g ≫
      ((F.shiftIso 1 n₀ n₁ ⋯).app T.obj₁).hom

Tactic:
simp [homologySequenceδ, shiftMap]

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.shift n₀).map T.rotate.mor₁) ((F.shift n₀).map T.rotate.mor₂) ⋯ ≅
    ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _)
  ((F.shiftIso 1 n₀ n₁ (by omega)).app _) (by simp) (by simp [homologySequenceδ, shiftMap])

Result:
no goals