awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : ChainComplex.{v, u, 0} C ℕ
inst_2 : ∀ (n : ℕ), Projective.{v, u} (K.X n)
inst_3 : ∀ (n : ℕ), Projective.{v, u} (L.X n)
f : K ⟶ L
rw :
  QuasiIso (K := extend K ComplexShape.embeddingDownNat) (extendMap f ComplexShape.embeddingDownNat) ↔
    homotopyEquivalences C (ComplexShape.down ℕ) f
rw₁ :
  homotopyEquivalences C (ComplexShape.up ℤ) (X := extend K ComplexShape.embeddingDownNat)
      (extendMap f ComplexShape.embeddingDownNat) ↔
    homotopyEquivalences C (ComplexShape.down ℕ) f
rw₂ rw₃ : homotopyEquivalences C (ComplexShape.down ℕ) f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f

Tactic:
rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingDownNat,
    CochainComplex.IsKProjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]

Premises used: CochainComplex.IsKProjective.quasiIso_iff, HomologicalComplex.quasiIso_extendMap_iff, ComplexShape.embeddingDownNat, HomologicalComplex.homotopyEquivalences_extendMap_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasDerivedCategory.{w, v, u} C
⊢ Functor.Linear R (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) (D := DerivedCategory.{w, v, u} C) Qh

Tactic:
Localization.functor_linear _ _ _

Premises used: CategoryTheory.Localization.functor_linear
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasDerivedCategory.{w, v, u} C
⊢ Functor.Linear R (C := CochainComplex.{v, u, 0} C ℤ) (D := DerivedCategory.{w, v, u} C) Q

Tactic:
Functor.linear_of_iso _ (quotientCompQhIso C)

Premises used: CategoryTheory.Functor.linear_of_iso, DerivedCategory.quotientCompQhIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Functor.Linear R (C := DerivedCategory.{w, v, u} C) (shiftFunctor (DerivedCategory.{w, v, u} C) n)

Tactic:
Shift.linear_of_localization R Qh (HomotopyCategory.subcategoryAcyclic C).trW _

Premises used: DerivedCategory.Qh, CategoryTheory.Shift.linear_of_localization, CategoryTheory.ObjectProperty.trW, HomotopyCategory.subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Linear
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasDerivedCategory.{w, v, u} C
n : ℤ
⊢ Functor.Linear R (D := DerivedCategory.{w, v, u} C) (singleFunctor C n)

Tactic:
inferInstanceAs (Functor.Linear R (HomotopyCategory.singleFunctor C n ⋙ Qh))

Premises used: _private.0.DerivedCategory.instLinearSingleFunctor._proof_1
-- 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
⊢ 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.descShortComplex S) ≫ triangleOfSESδ hS)
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso Q 1)) S.X₁)

Tactic:
simp [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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
simp :
  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)
          (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁) ≫
      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) (Functor.obj Q S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj Q S₂.X₁)))
    (triangleOfSESδ hS₁ ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (CategoryTheory.Functor.map Q f.τ₁))
    (CategoryTheory.Functor.map Q f.τ₃ ≫ triangleOfSESδ hS₂)

Tactic:
simp only [triangleOfSESδ, CochainComplex.mappingCone.triangle_obj₁, Category.assoc,
    IsIso.inv_comp_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, DerivedCategory.triangleOfSESδ, CochainComplex.mappingCone.triangle_obj₁
-- 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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : 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 (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1 ⋙ Q) S₂.X₁))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1 ⋙ Q) f.τ₁)
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁ ≫ f.τ₃) ≫
        inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₂))) ≫
      CategoryTheory.Functor.map Q (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₃ ≫
      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 (CochainComplex.mappingCone.descShortComplex S₁) ≫
      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 [← Functor.comp_map, ← (Q.commShiftIso (1 : ℤ)).hom.naturality, ← Category.assoc,
    ← Category.assoc, ← Category.assoc, ← Category.assoc, ← Iso.app_hom,
    Iso.cancel_iso_hom_right, ← Q.map_comp]

Premises used: CategoryTheory.Category.assoc, DerivedCategory.Q, CategoryTheory.Iso.app_hom, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.cancel_iso_hom_right, CategoryTheory.Functor.map_comp, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.Functor.comp_map
-- 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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
simp :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
      (Functor.obj Q (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) S₂.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map Q
        (CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁))
    (CategoryStruct.comp (Y := Functor.obj Q (CochainComplex.mappingCone S₂.f))
      (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) :
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
          (Functor.obj Q (CochainComplex.mappingCone S₂.f)))
      (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃ :
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₂.f))
          (Functor.obj Q (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) S₂.X₁))))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1 ⋙ Q) S₂.X₁))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1 ⋙ Q) f.τ₁)
    ((CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₁ ≫ f.τ₃) ≫
        inv (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S₂))) ≫
      CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃)

Tactic:
simp only [Functor.comp_obj, Functor.comp_map,
    ← CochainComplex.mappingCone.descShortComplex_naturality f,
    Functor.map_comp, Category.assoc, IsIso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CochainComplex.mappingCone.descShortComplex_naturality, CategoryTheory.Functor.map_comp, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Functor.comp_map
-- 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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : 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 Q (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) S₂.X₁)))
    (CategoryTheory.Functor.map Q
      ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
        CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁))
    (CategoryTheory.Functor.map Q
      (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 Q (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) S₂.X₁)))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
      CategoryTheory.Functor.map Q
        (CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁))
    (CategoryStruct.comp (Y := Functor.obj Q (CochainComplex.mappingCone S₂.f))
      (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) :
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₁.f))
          (Functor.obj Q (CochainComplex.mappingCone S₂.f)))
      (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.triangle S₂.f).mor₃ :
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (CochainComplex.mappingCone S₂.f))
          (Functor.obj Q (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) S₂.X₁))))

Tactic:
rw [← Q.map_comp, ← Q.map_comp]

Premises used: DerivedCategory.Q, 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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : 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 Q (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) S₂.X₁)))
    (CategoryTheory.Functor.map Q
      ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫
        CategoryTheory.Functor.map (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) (A := ℤ) 1) f.τ₁))
    (CategoryTheory.Functor.map Q
      (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃))

Tactic:
congr 1
-- 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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : 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₁ S₂ : ShortComplex (CochainComplex.{v, u, 0} C ℤ)
hS₁ : S₁.ShortExact
hS₂ : 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.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
⊢ QuasiIso (CochainComplex.mappingCone.descShortComplex S)

Tactic:
have := CochainComplex.mappingCone.quasiIso_descShortComplex 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
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
refine_1 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Triangle.obj₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
      (Triangle.obj₂ (triangleOfSES hS)))
    (Triangle.mor₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)) ≫
      Iso.hom
        (Iso.refl (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))))
    (Iso.hom
        (Iso.refl (Triangle.obj₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))) ≫
      Triangle.mor₁ (triangleOfSES hS))
refine_2 :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
      (Triangle.obj₃ (triangleOfSES hS)))
    (Triangle.mor₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)) ≫
        Iso.hom (asIso (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S))) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C)
        (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
        (Triangle.obj₃ (triangleOfSES hS)))
    (Iso.hom
          (Iso.refl (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))) ≫
        Triangle.mor₂ (triangleOfSES hS) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C)
        (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
        (Triangle.obj₃ (triangleOfSES hS)))
refine_3 :
  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))
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
    (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f))

Tactic:
refine Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_ ?_ ?_)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.Iso.symm, CategoryTheory.asIso
-- 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_1 :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S.X₁) (Functor.obj Q S.X₂))
    (CategoryTheory.Functor.map Q S.f ≫ 𝟙 (Functor.obj Q S.X₂))
    (𝟙 (Functor.obj Q S.X₁) ≫ CategoryTheory.Functor.map Q S.f)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Triangle.obj₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
      (Triangle.obj₂ (triangleOfSES hS)))
    (Triangle.mor₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)) ≫
      Iso.hom
        (Iso.refl (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))))
    (Iso.hom
        (Iso.refl (Triangle.obj₁ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))) ≫
      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
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S.X₁) (Functor.obj Q S.X₂))
    (CategoryTheory.Functor.map Q S.f ≫ 𝟙 (Functor.obj Q S.X₂))
    (𝟙 (Functor.obj Q S.X₁) ≫ CategoryTheory.Functor.map Q S.f)

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_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
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
refine_2 :
  Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S.X₂) (Functor.obj Q S.X₃))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.inr S.f) ≫
      CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S))
    (𝟙 (Functor.obj Q S.X₂) ≫ CategoryTheory.Functor.map Q S.g)
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
      (Triangle.obj₃ (triangleOfSES hS)))
    (Triangle.mor₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)) ≫
        Iso.hom (asIso (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S))) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C)
        (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
        (Triangle.obj₃ (triangleOfSES hS)))
    (Iso.hom
          (Iso.refl (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))) ≫
        Triangle.mor₂ (triangleOfSES hS) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C)
        (Triangle.obj₂ (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f)))
        (Triangle.obj₃ (triangleOfSES hS)))

Tactic:
dsimp
-- 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)
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q S.X₂) (Functor.obj Q S.X₃))
    (CategoryTheory.Functor.map Q (CochainComplex.mappingCone.inr S.f) ≫
      CategoryTheory.Functor.map Q (CochainComplex.mappingCone.descShortComplex S))
    (𝟙 (Functor.obj Q S.X₂) ≫ CategoryTheory.Functor.map Q S.g)

Tactic:
simp only [← Q.map_comp, CochainComplex.mappingCone.inr_descShortComplex, id_comp]

Premises used: DerivedCategory.Q, CochainComplex.mappingCone.inr_descShortComplex, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp