awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.IsLocalization (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh
    (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh

Tactic:
Localization.functor_additive Qh (HomotopyCategory.subcategoryAcyclic C).trW

Premises used: DerivedCategory.Qh, CategoryTheory.ObjectProperty.trW, HomotopyCategory.subcategoryAcyclic, CategoryTheory.Localization.functor_additive
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.Additive (C := CochainComplex.{v, u, 0} C ℤ) (D := DerivedCategory.{w, v, u} C) Q

Tactic:
Functor.additive_of_iso (quotientCompQhIso C)

Premises used: CategoryTheory.Functor.additive_of_iso, DerivedCategory.quotientCompQhIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ HasZeroObject (DerivedCategory.{w, v, u} C)

Tactic:
Q.hasZeroObject_of_additive

Premises used: DerivedCategory.Q, CategoryTheory.Functor.hasZeroObject_of_additive
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ NatTrans.CommShift (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C)
    (Iso.hom (quotientCompQhIso C)) ℤ

Tactic:
Functor.CommShift.ofIso_compatibility (quotientCompQhIso C) ℤ

Premises used: Int, CategoryTheory.Functor.CommShift.ofIso_compatibility, DerivedCategory.quotientCompQhIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
rw :
  Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C)
    (Qh ⋙ shiftFunctor (DerivedCategory.{w, v, u} C) n)
⊢ Functor.Additive (C := DerivedCategory.{w, v, u} C) (shiftFunctor (DerivedCategory.{w, v, u} C) n)

Tactic:
rw [Localization.functor_additive_iff
    Qh (HomotopyCategory.subcategoryAcyclic C).trW]

Premises used: DerivedCategory.Qh, CategoryTheory.Localization.functor_additive_iff, CategoryTheory.ObjectProperty.trW, HomotopyCategory.subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C)
    (Qh ⋙ shiftFunctor (DerivedCategory.{w, v, u} C) n)

Tactic:
Functor.additive_of_iso (Qh.commShiftIso n)

Premises used: DerivedCategory.Qh, CategoryTheory.Functor.additive_of_iso, CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Functor.Additive (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C)
    (Qh ⋙ shiftFunctor (DerivedCategory.{w, v, u} C) n)

Tactic:
exact Functor.additive_of_iso (Qh.commShiftIso n)

Premises used: DerivedCategory.Qh, CategoryTheory.Functor.additive_of_iso, CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.IsTriangulated (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh

Tactic:
Triangulated.Localization.isTriangulated_functor
    Qh (HomotopyCategory.subcategoryAcyclic C).trW

Premises used: DerivedCategory.Qh, CategoryTheory.Triangulated.Localization.isTriangulated_functor, CategoryTheory.ObjectProperty.trW, HomotopyCategory.subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ IsTriangulated (DerivedCategory.{w, v, u} C)

Tactic:
Triangulated.Localization.isTriangulated
    Qh (HomotopyCategory.subcategoryAcyclic C).trW

Premises used: DerivedCategory.Qh, CategoryTheory.Triangulated.Localization.isTriangulated, CategoryTheory.ObjectProperty.trW, HomotopyCategory.subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.EssSurj (C := Arrow (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))) (D :=
    Arrow (DerivedCategory.{w, v, u} C)) (Functor.mapArrow Qh)

Tactic:
Localization.essSurj_mapArrow _ (HomotopyCategory.subcategoryAcyclic C).trW

Premises used: CategoryTheory.ObjectProperty.trW, HomotopyCategory.subcategoryAcyclic, CategoryTheory.Localization.essSurj_mapArrow
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
⊢ Functor.Full (C := DerivedCategory.{w, v, u} C ⥤ D)
    (Functor.obj
      (Functor.whiskeringLeft (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (DerivedCategory.{w, v, u} C) D) Qh)

Tactic:
inferInstanceAs
    (Localization.whiskeringLeftFunctor' _ (HomotopyCategory.quasiIso _ _) D).Full

Premises used: _private.0.DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh._proof_1
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
D : Type u_1
inst_3 : Category.{v_1, u_1} D
⊢ Functor.Faithful (C := DerivedCategory.{w, v, u} C ⥤ D)
    (Functor.obj
      (Functor.whiskeringLeft (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (DerivedCategory.{w, v, u} C) D) Qh)

Tactic:
inferInstanceAs
    (Localization.whiskeringLeftFunctor' _ (HomotopyCategory.quasiIso _ _) D).Faithful

Premises used: _private.0.DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh._proof_1
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.EssSurj (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh

Tactic:
Localization.essSurj _ (HomotopyCategory.quasiIso _ _)

Premises used: CategoryTheory.Localization.essSurj, HomotopyCategory.quasiIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ Functor.EssSurj (C := CochainComplex.{v, u, 0} C ℤ) (D := DerivedCategory.{w, v, u} C) Q

Tactic:
Localization.essSurj _ (HomologicalComplex.quasiIso _ _)

Premises used: CategoryTheory.Localization.essSurj, HomologicalComplex.quasiIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
mp :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T →
    ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
      Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))
mpr :
  (∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
      Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))) →
    Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T ↔
    ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
      Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
T' : Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
e : T ≅ Functor.obj (Functor.mapTriangle Qh) T'
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))

Tactic:
⟨_, _, f, ⟨?_⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
T' : Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
e : T ≅ Functor.obj (Functor.mapTriangle Qh) T'
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
mp : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
⊢ ∃ (X : CochainComplex.{v, u, 0} C ℤ) (Y : CochainComplex.{v, u, 0} C ℤ) (f : X ⟶ Y),
    Nonempty.{w + 1} (T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f))

Tactic:
refine ⟨_, _, f, ⟨?_⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
T' : Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
e : T ≅ Functor.obj (Functor.mapTriangle Qh) T'
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e' : T' ≅ CochainComplex.mappingCone.triangleh f
⊢ T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)

Tactic:
exact e ≪≫ Qh.mapTriangle.mapIso e' ≪≫
      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).symm.app _ ≪≫
      (Functor.mapTriangleIso (quotientCompQhIso C)).app _

Premises used: CategoryTheory.Functor.mapTriangleIso, DerivedCategory.Qh, CategoryTheory.Functor.mapTriangle, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, HomotopyCategory.quotient, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T

Tactic:
isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
      (e ≪≫ (Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)

Premises used: CategoryTheory.Functor.mapTriangleIso, DerivedCategory.Qh, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, HomotopyCategory.quotient, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.app, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
mpr :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (HomotopyCategory.instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (Functor.obj (Functor.mapTriangle (HomotopyCategory.quotient C (ComplexShape.up ℤ)))
      (CochainComplex.mappingCone.triangle f))
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T

Tactic:
refine isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
      (e ≪≫ (Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)

Premises used: CategoryTheory.Functor.mapTriangleIso, DerivedCategory.Qh, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapTriangleCompIso, HomotopyCategory.quotient, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.app, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (HomotopyCategory.instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (Functor.obj (Functor.mapTriangle (HomotopyCategory.quotient C (ComplexShape.up ℤ)))
      (CochainComplex.mappingCone.triangle f))

Tactic:
⟨_, _, f, ⟨Iso.refl _⟩⟩

Premises used: Set.Mem, setOf, CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (DerivedCategory.{w, v, u} C)
X Y : CochainComplex.{v, u, 0} C ℤ
f : X ⟶ Y
e : T ≅ Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle f)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (HomotopyCategory.instPreadditive C (ComplexShape.up ℤ)) ⋯ _)
    (Functor.obj (Functor.mapTriangle (HomotopyCategory.quotient C (ComplexShape.up ℤ)))
      (CochainComplex.mappingCone.triangle f))

Tactic:
exact ⟨_, _, f, ⟨Iso.refl _⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
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)) (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle φ))
        (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle f)))
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle φ))

Tactic:
rw [mem_distTriang_iff]

Premises used: DerivedCategory.mem_distTriang_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
⊢ ∃ (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)) (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle φ))
        (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle f)))

Tactic:
⟨_, _, _, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
⊢ ∃ (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)) (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle φ))
        (Functor.obj (Functor.mapTriangle Q) (mappingCone.triangle f)))

Tactic:
exact ⟨_, _, _, ⟨Iso.refl _⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
rw :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _)
    (Triangle.rotate (Functor.obj (Functor.mapTriangle Q) (mappingCocone.triangle φ)))
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle Q) (mappingCocone.triangle φ))

Tactic:
rw [rotate_distinguished_triangle]

Premises used: CategoryTheory.Pretriangulated.rotate_distinguished_triangle
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _)
    (Triangle.rotate (Functor.obj (Functor.mapTriangle Q) (mappingCocone.triangle φ)))

Tactic:
isomorphic_distinguished _ (mappingCone_triangle_distinguished φ) _
    (DerivedCategory.Q.mapTriangleRotateIso.app _ ≪≫
    DerivedCategory.Q.mapTriangle.mapIso (mappingCocone.rotateTriangleIso φ))

Premises used: CochainComplex.mappingCocone.rotateTriangleIso, DerivedCategory.mappingCone_triangle_distinguished, DerivedCategory.Q, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.mapTriangleRotateIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
⊢ Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _)
    (Triangle.rotate (Functor.obj (Functor.mapTriangle Q) (mappingCocone.triangle φ)))

Tactic:
exact isomorphic_distinguished _ (mappingCone_triangle_distinguished φ) _
    (DerivedCategory.Q.mapTriangleRotateIso.app _ ≪≫
    DerivedCategory.Q.mapTriangle.mapIso (mappingCocone.rotateTriangleIso φ))

Premises used: CochainComplex.mappingCocone.rotateTriangleIso, DerivedCategory.mappingCone_triangle_distinguished, DerivedCategory.Q, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.trans, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.mapTriangleRotateIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Functor.Additive (D := DerivedCategory.{w, v, u} C)
    (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n ⋙ Qh)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq (α := DerivedCategory.{w, v, u} C)
    (Functor.obj Qh (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X))
    (Functor.obj (singleFunctor C n) X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq (α := DerivedCategory.{w, v, u} C)
    (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) X))
    (Functor.obj (singleFunctor C n) X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
w :
  ∀ (X : C),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X))
      (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) n) X)
      (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors C) n)) X)
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ DerivedCategory.{w, v, u} C) (SingleFunctors.functor (singleFunctors C) n)
      (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n))
    (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) n)
    (𝟙 (SingleFunctors.functor (singleFunctors C) n))

Tactic:
ext X
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
w :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
        𝟙 (Functor.obj (singleFunctor C n) X) ≫
          𝟙
            (Functor.obj HomologicalComplexUpToQuasiIso.Q
              (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) n) X)
    (NatTrans.app (𝟙 (SingleFunctors.functor (singleFunctors C) n)) X)

Tactic:
dsimp [singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso,
    quotientCompQhIso, HomologicalComplexUpToQuasiIso.quotientCompQhIso]

Premises used: DerivedCategory.singleFunctorsPostcompQIso, HomologicalComplexUpToQuasiIso.quotientCompQhIso, DerivedCategory.quotientCompQhIso, HomotopyCategory.singleFunctorsPostcompQuotientIso