-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma homologySequence_exact₂ :
    (ShortComplex.mk _ _ (F.homologySequence_comp T hT n₀)).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₀ : ℤ
⊢ (shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F ≅
    ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯

Tactic:
exact ShortComplex.isoMk ((F.isoShift n₀).app _)
  (n₀.negOnePow • ((F.isoShift n₀).app _)) ((F.isoShift n₀).app _)
  (by dsimp; simp) (by dsimp; 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₀ : ℤ
⊢ (ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯).Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.map_distinguished_exact _
  (Triangle.shift_distinguished _ 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₀ : ℤ
⊢ (shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F ≅
    ShortComplex.mk ((F.shift n₀).map T.mor₁) ((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₀ : ℤ
⊢ ((F.isoShift n₀).app T.obj₁).hom ≫ (ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯).f =
    ((shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F).f ≫
      (n₀.negOnePow • (F.isoShift n₀).app T.obj₂).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₀ : ℤ
⊢ (F.isoShift n₀).hom.app T.obj₁ ≫ (F.shift n₀).map T.mor₁ =
    F.map (n₀.negOnePow • (shiftFunctor C n₀).map T.mor₁) ≫ (n₀.negOnePow • (F.isoShift n₀).hom.app 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₀.negOnePow • (F.isoShift n₀).app T.obj₂).hom ≫
      (ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯).g =
    ((shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F).g ≫ ((F.isoShift n₀).app T.obj₃).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₀.negOnePow • (F.isoShift n₀).hom.app T.obj₂) ≫ (F.shift n₀).map T.mor₂ =
    F.map (n₀.negOnePow • (shiftFunctor C n₀).map T.mor₂) ≫ (F.isoShift n₀).hom.app 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₀.negOnePow • (F.isoShift n₀).hom.app T.obj₂) ≫ (F.shift n₀).map T.mor₂ =
    F.map (n₀.negOnePow • (shiftFunctor C n₀).map T.mor₂) ≫ (F.isoShift n₀).hom.app T.obj₃

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₀ : ℤ
⊢ (F.isoShift n₀).hom.app T.obj₁ ≫ (F.shift n₀).map T.mor₁ =
    F.map (n₀.negOnePow • (shiftFunctor C n₀).map T.mor₁) ≫ (n₀.negOnePow • (F.isoShift n₀).hom.app T.obj₂)

Tactic:
simp

Result:
no goals