awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
refine_3 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S.X₁)))
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (𝟙 (Functor.obj Q S.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S) ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Triangle.obj₃ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Triangle.obj₁ (triangleOfSES hS))))
    (Triangle.mor₃ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (Iso.hom
          (Iso.refl (Triangle.obj₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f))))))
    (Iso.hom (asIso (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S))) ≫
      Triangle.mor₃ (triangleOfSES hS))

Tactic:
dsimp [triangleOfSESδ]

Premises used: DerivedCategory.triangleOfSESδ
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
rw :
  ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1}
      (Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
        (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)))
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (triangleOfSES hS)

Tactic:
rw [mem_distTriang_iff]

Premises used: DerivedCategory.mem_distTriang_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
⊢ ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1}
      (Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
        (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)))

Tactic:
⟨_, _, S.f, ⟨triangleOfSESIso hS⟩⟩

Premises used: DerivedCategory.triangleOfSESIso, Nonempty.intro, Exists.intro, CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
⊢ ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1}
      (Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
        (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)))

Tactic:
exact ⟨_, _, S.f, ⟨triangleOfSESIso hS⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₁ (triangleOfSES h₁)) (Triangle.obj₂ (triangleOfSES h₂)))
    (Triangle.mor₁ (triangleOfSES h₁) ≫ CategoryTheory.Functor.map Q f.τ₂)
    (CategoryTheory.Functor.map Q f.τ₁ ≫ Triangle.mor₁ (triangleOfSES h₂))

Tactic:
simp [← Functor.map_comp, f.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₂ (triangleOfSES h₁)) (Triangle.obj₃ (triangleOfSES h₂)))
    (Triangle.mor₂ (triangleOfSES h₁) ≫ CategoryTheory.Functor.map Q f.τ₃)
    (CategoryTheory.Functor.map Q f.τ₂ ≫ Triangle.mor₂ (triangleOfSES h₂))

Tactic:
simp [← Functor.map_comp, f.comm₂₃]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
dsimp :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    ((inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₁.X₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q f.τ₃ ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₂)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ (triangleOfSES h₁))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Triangle.obj₁ (triangleOfSES h₂))))
    (Triangle.mor₃ (triangleOfSES h₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q f.τ₃ ≫ Triangle.mor₃ (triangleOfSES h₂))

Tactic:
dsimp [triangleOfSES, triangleOfSESδ]

Premises used: DerivedCategory.triangleOfSESδ, DerivedCategory.triangleOfSES
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    (CategoryTheory.Functor.map Q
        ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
    (CategoryTheory.Functor.map Q
        (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    ((inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₁.X₁) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q f.τ₃ ≫
      inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₂)) ≫
        CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)

Tactic:
rw [assoc, assoc, IsIso.inv_comp_eq, ← Functor.map_comp_assoc,
      ← CochainComplex.mappingCone.map_descShortComplex,
      Functor.map_comp_assoc, IsIso.hom_inv_id_assoc,
      ← Functor.commShiftIso_hom_naturality,
      ← Functor.map_comp_assoc, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Functor.commShiftIso_hom_naturality, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Functor.map_comp_assoc, CochainComplex.mappingCone.map_descShortComplex
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
e_a :
  (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁ =
    CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    (CategoryTheory.Functor.map Q
        ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)
    (CategoryTheory.Functor.map Q
        (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S₂.X₁)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁ =
    CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃

Tactic:
(CochainComplex.mappingCone.triangleMap S₁.f S₂.f f.τ₁ f.τ₂ f.comm₁₂.symm).comm₃

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CochainComplex.mappingCone.triangleMap, CochainComplex.mappingCone, CochainComplex.mappingCone.map, CochainComplex.HomComplex.Cocycle.homOf, CategoryTheory.ShortComplex.Hom.τ₂, HomologicalComplex.homotopyCofiber, CategoryTheory.ShortComplex.f, CochainComplex.mappingCone.desc, Eq.symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁ =
    CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃

Tactic:
exact (CochainComplex.mappingCone.triangleMap S₁.f S₂.f f.τ₁ f.τ₂ f.comm₁₂.symm).comm₃

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CochainComplex.mappingCone.triangleMap, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.f, Eq.symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
e : Iso (C := C ⥤ DerivedCategory.{w, v, u} C)
  (Functor.obj (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctors C))
  (Functor.obj (C := SingleFunctors C (DerivedCategory.{w, v, u} C) ℤ)
    (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0)
    (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q)) :=
  Functor.mapIso (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctorsPostcompQIso C)
refine_1 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₁ hS.singleTriangle)
      (Triangle.obj₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)))
    (Triangle.mor₁ hS.singleTriangle ≫ Iso.hom (e.app S.X₂))
    (Iso.hom (e.app S.X₁) ≫
      Triangle.mor₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))
refine_2 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₂ hS.singleTriangle)
      (Triangle.obj₃ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)))
    (Triangle.mor₂ hS.singleTriangle ≫ Iso.hom (e.app S.X₃))
    (Iso.hom (e.app S.X₂) ≫
      Triangle.mor₂ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))
refine_3 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ hS.singleTriangle)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (Triangle.obj₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))))
    (Triangle.mor₃ hS.singleTriangle ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Iso.hom (e.app S.X₁)))
    (Iso.hom (e.app S.X₃) ≫
      Triangle.mor₃ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) hS.singleTriangle
    (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯)

Tactic:
refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
e : Iso (C := C ⥤ DerivedCategory.{w, v, u} C)
  (Functor.obj (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctors C))
  (Functor.obj (C := SingleFunctors C (DerivedCategory.{w, v, u} C) ℤ)
    (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0)
    (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q)) :=
  Functor.mapIso (SingleFunctors.evaluation C (DerivedCategory.{w, v, u} C) 0) (singleFunctorsPostcompQIso C)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ hS.singleTriangle)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (Triangle.obj₁ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))))
    (Triangle.mor₃ hS.singleTriangle ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Iso.hom (e.app S.X₁)))
    (Iso.hom (e.app S.X₃) ≫
      Triangle.mor₃ (triangleOfSES (S := S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) ⋯))

Tactic:
simp [singleδ, e, ← Functor.map_comp, CochainComplex.singleFunctors]

Premises used: CategoryTheory.ShortComplex.ShortExact.singleδ, CochainComplex.singleFunctors, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _) hS.singleTriangle

Tactic:
isomorphic_distinguished _ (triangleOfSES_distinguished (hS.map_of_exact
    (HomologicalComplex.single C (ComplexShape.up ℤ) 0))) _ (singleTriangleIso hS)

Premises used: Int, CategoryTheory.Pretriangulated.isomorphic_distinguished, DerivedCategory.triangleOfSES_distinguished, OfNat.ofNat, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso, CategoryTheory.ShortComplex.ShortExact.map_of_exact, ComplexShape.up, HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₁ h₁.singleTriangle) (Triangle.obj₂ h₂.singleTriangle))
    (Triangle.mor₁ h₁.singleTriangle ≫ Functor.map (singleFunctor C 0) f.τ₂)
    (Functor.map (singleFunctor C 0) f.τ₁ ≫ Triangle.mor₁ h₂.singleTriangle)

Tactic:
simp [← Functor.map_comp, f.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₂ h₁.singleTriangle) (Triangle.obj₃ h₂.singleTriangle))
    (Triangle.mor₂ h₁.singleTriangle ≫ Functor.map (singleFunctor C 0) f.τ₃)
    (Functor.map (singleFunctor C 0) f.τ₂ ≫ Triangle.mor₂ h₂.singleTriangle)

Tactic:
simp [← Functor.map_comp, f.comm₂₃]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
dsimp :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    ((NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₁.X₁)) ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.map (singleFunctor C 0) f.τ₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Triangle.obj₃ h₁.singleTriangle)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Triangle.obj₁ h₂.singleTriangle)))
    (Triangle.mor₃ h₁.singleTriangle ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.map (singleFunctor C 0) f.τ₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫ Triangle.mor₃ h₂.singleTriangle)

Tactic:
dsimp [singleδ]

Premises used: CategoryTheory.ShortComplex.ShortExact.singleδ
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.map (SingleFunctors.functor (CochainComplex.singleFunctors C) 0 ⋙ Q) f.τ₁) ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    ((NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₁.X₁)) ≫
      Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.map (singleFunctor C 0) f.τ₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))

Tactic:
rw [assoc, assoc, ← Functor.map_comp, ← NatTrans.naturality, Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp