awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f
have rw₂ : homotopyEquivalences C (ComplexShape.down ℕ) f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f
Tactic: rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingDownNat,
    CochainComplex.IsKProjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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₂
⊢ 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₂)
have 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₁)
Tactic: simp only [triangleOfSESδ, CochainComplex.mappingCone.triangle_obj₁, Category.assoc,
    IsIso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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₂
⊢ 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₁)
have 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₃)
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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₂
⊢ 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₃)
have 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.τ₂ sorry) :
      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: 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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₂
⊢ 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₁))))
have 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.τ₂ sorry ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃))
Tactic: rw [← Q.map_comp, ← Q.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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₂
⊢ 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₃))
have 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.τ₂ sorry ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (hypothesis)
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
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
    (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f))
have this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
Tactic: have := CochainComplex.mappingCone.quasiIso_descShortComplex hS
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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)
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
    (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f))
have 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))
Tactic: refine Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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))
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
    (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f))
have 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)))
Tactic: refine Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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)))
⊢ Iso (C := Triangle (DerivedCategory.{w, v, u} C)) (triangleOfSES hS)
    (Functor.obj (Functor.mapTriangle Q) (CochainComplex.mappingCone.triangle S.f))
have 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))
Tactic: refine Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))) ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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)
      (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))
have 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)
Tactic: dsimp [triangleOfSES]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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)
      (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)))
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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)
      (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))
have 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₁)
Tactic: dsimp [triangleOfSESδ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.ShortExact (goal)
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 (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₁)
have 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₁) ≫
    𝟙 (Functor.obj (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₁)
Tactic: rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]