awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀ : ℤ
⊢ Eq (α :=
    ShortComplex.X₂ ((shortComplexOfDistTriangle (obj (shiftFunctor (Triangle.{v_1, u_1} C) n₀) T) ⋯).map F) ⟶
      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 := ⋯ })
    ((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 ≫
      ShortComplex.g
        { 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.g ((shortComplexOfDistTriangle (obj (shiftFunctor (Triangle.{v_1, u_1} C) n₀) T) ⋯).map F) ≫
      Iso.hom (Iso.app (F.isoShift n₀) T.obj₃))

Tactic:
simp
-- 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₀ : ℤ
⊢ 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 := ⋯ }

Tactic:
exact ShortComplex.isoMk ((F.isoShift n₀).app _)
    (n₀.negOnePow • ((F.isoShift n₀).app _)) ((F.isoShift n₀).app _)
    (by simp) (by simp)

Premises used: CategoryTheory.ShortComplex.isoMk
-- 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₁
⊢ 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 := ⋯ }

Tactic:
ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (rot_of_distTriang _ hT) n₀)

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Pretriangulated.rot_of_distTriang
-- 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₁
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 := ⋯ }
    { 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 := ⋯ }
⊢ 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 := ⋯ }

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (rot_of_distTriang _ hT) n₀)

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Pretriangulated.rot_of_distTriang
-- 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₁
⊢ 1 + n₀ = n₁

Tactic:
lia
-- 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₁
⊢ Iso.hom
        (Iso.refl
          (ShortComplex.X₁
            { 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 := ⋯ : ShortComplex.{v_3, u_3} A })) ≫
      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.homologySequenceδ T n₀ n₁ h, zero := ⋯ : ShortComplex.{v_3, u_3} A } =
    ShortComplex.f
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₂
            { 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 := ⋯ }))

Tactic:
simp
-- 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₁
⊢ Iso.hom
        (Iso.refl
          (ShortComplex.X₂
            { 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 := ⋯ : ShortComplex.{v_3, u_3} A })) ≫
      ShortComplex.g
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } =
    ShortComplex.g
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } ≫
      Iso.hom (Iso.app (F.shiftIso 1 n₀ n₁ ⋯) T.obj₁)

Tactic:
simp [homologySequenceδ, shiftMap]

Premises used: CategoryTheory.Functor.shiftMap, 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₁
⊢ 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 := ⋯ }
    { 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 := ⋯ }

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.isoMk
-- 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₁
⊢ 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 := ⋯ }

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

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Pretriangulated.inv_rot_of_distTriang
-- 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₁
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 := ⋯ }
    { 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 := ⋯ }
⊢ 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 := ⋯ }

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

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Pretriangulated.inv_rot_of_distTriang
-- 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₁
⊢ -1 + n₁ = n₀

Tactic:
lia
-- 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₁
⊢ Iso.hom
        (Iso.refl
          (ShortComplex.X₂
            { 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 := ⋯ : ShortComplex.{v_3, u_3} A })) ≫
      ShortComplex.g
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } =
    ShortComplex.g
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₃
            { 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 := ⋯ }))

Tactic:
simp
-- 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₁
refine :
  Iso.hom (-Iso.app (F.shiftIso (-1) n₁ 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.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ } =
    ShortComplex.f
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₂
            { 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 := ⋯ : ShortComplex.{v_3, u_3} A }))
⊢ 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 := ⋯ }
    { 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 := ⋯ }

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.isoMk
-- 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 :
  Eq (α := (F.shift n₁).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) T.obj₃) ⟶ (F.shift n₁).obj T.obj₁)
    ((-NatTrans.app (Iso.hom (F.shiftIso (-1) n₁ n₀ ⋯)) T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h)
    ((F.shift n₁).map
        (-map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T.obj₁) ≫
      𝟙 ((F.shift n₁).obj T.obj₁))
⊢ Iso.hom (-Iso.app (F.shiftIso (-1) n₁ 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.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ } =
    ShortComplex.f
        { 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 := ⋯ : ShortComplex.{v_3, u_3} A } ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₂
            { 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 := ⋯ : ShortComplex.{v_3, u_3} A }))

Tactic:
dsimp
-- 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₁
⊢ Eq (α := (F.shift n₁).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) T.obj₃) ⟶ (F.shift n₁).obj T.obj₁)
    ((-NatTrans.app (Iso.hom (F.shiftIso (-1) n₁ n₀ ⋯)) T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h)
    ((F.shift n₁).map
        (-map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) 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 lia)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.homologySequenceδ, neg_add_cancel, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Pretriangulated.Triangle.mor₃, CategoryTheory.Functor.map_neg, OfNat.ofNat, CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, Neg.neg
-- 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₀ : ℤ
⊢ Epi ((F.shift n₀).map T.mor₁) ↔ (F.shift n₀).map T.mor₂ = 0

Tactic:
(F.homologySequence_exact₂ T hT n₀).epi_f_iff

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ShortComplex.Exact.epi_f_iff
-- 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₁
⊢ Mono ((F.shift n₁).map T.mor₁) ↔
    Eq (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₁) (F.homologySequenceδ T n₀ n₁ h) 0

Tactic:
(F.homologySequence_exact₁ T hT n₀ n₁ h).mono_g_iff

Premises used: CategoryTheory.Functor.shiftMap, CategoryTheory.ShortComplex.Exact.mono_g_iff, CategoryTheory.Functor.homologySequenceδ, CategoryTheory.Functor.homologySequence_exact₁