awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Eq (α := ShiftedHom (C := DerivedCategory C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L) n)
    (CategoryStruct.comp (Y :=
        Functor.obj DerivedCategory.Q (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
        (CategoryTheory.Functor.map DerivedCategory.Q
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            y₁))
        (NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q n)) L) :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q K)
        (Functor.obj (CategoryTheory.shiftFunctor (DerivedCategory C) n) (Functor.obj DerivedCategory.Q L)))
    (CategoryStruct.comp (Y :=
        Functor.obj DerivedCategory.Q (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
        (CategoryTheory.Functor.map DerivedCategory.Q
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            y₂))
        (NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q n)) L) :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q K)
        (Functor.obj (CategoryTheory.shiftFunctor (DerivedCategory C) n) (Functor.obj DerivedCategory.Q L)))
have h₁ : Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
  Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
  ((AddEquiv.symm Cocycle.equivHomShift :
      (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
    y₁)
  ((AddEquiv.symm Cocycle.equivHomShift :
      (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
    y₂)
Tactic: rw [cancel_mono, DerivedCategory.Q_map_eq_of_homotopy]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
    Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      y₁)
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      y₂)
have h₁ : Eq.{max 1 (v + 1)} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      y₁))
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      y₂))
Tactic: apply HomotopyCategory.homotopyOfEq
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Eq.{max 1 (v + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        y₁))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        y₂))
have h₁ : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
  ((toHom :
        (a : CohomologyClass K L n) →
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
      (mk y₁) :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
  ((toHom :
        (a : CohomologyClass K L n) →
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
      (mk y₂) :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
Tactic: rw [← toHom_mk, ← toHom_mk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk y₁) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk y₂) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
have h₁ : mk y₁ = mk y₂
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X Y : DerivedCategory.{w, v, u} C
f : X ⟶ Y
K : CochainComplex.{v, u, 0} C ℤ
e₁ : X ≅ Functor.obj Q K
h : K.IsStrictlyLE 0
L : CochainComplex.{v, u, 0} C ℤ
e₂ : Y ≅ Functor.obj Q L
h_1 : L.IsStrictlyGE 1
⊢ f = 0
have rw : (e₁.inv ≫ f) ≫ e₂.hom = 0
Tactic: rw [← cancel_epi e₁.inv, ← cancel_mono e₂.hom, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
⊢ ∃ (X_1 : DerivedCategory.{w, v, u} C) (Y : DerivedCategory.{w, v, u} C) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : X_1 ≅ Functor.obj Q K), K.IsStrictlyLE 0) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyGE 1) (f : X_1 ⟶ X) (g : X ⟶ Y) (h :
    Y ⟶ Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) X_1),
    Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (Triangle.mk f g h)
have obtain : ∀ (K : CochainComplex.{v, u, 0} C ℤ) (e₂ : Functor.obj Q K ≅ X),
  ∃ (X_1 : DerivedCategory.{w, v, u} C) (Y : DerivedCategory.{w, v, u} C) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : X_1 ≅ Functor.obj Q K), K.IsStrictlyLE 0) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyGE 1) (f : X_1 ⟶ X) (g : X ⟶ Y) (h :
    Y ⟶ Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) X_1),
    Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ sorry _ instPreadditive sorry _) (Triangle.mk f g h)
Tactic: obtain ⟨K, ⟨e₂⟩⟩ : ∃ K, Nonempty (Q.obj K ≅ X) := ⟨_, ⟨Q.objObjPreimageIso X⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
⊢ ∃ (X_1 : DerivedCategory.{w, v, u} C) (Y : DerivedCategory.{w, v, u} C) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : X_1 ≅ Functor.obj Q K), K.IsStrictlyLE 0) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyGE 1) (f : X_1 ⟶ X) (g : X ⟶ Y) (h :
    Y ⟶ Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) X_1),
    Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (Triangle.mk f g h)
have h : (K.shortComplexTruncLE 0).ShortExact
Tactic: have h := K.shortComplexTruncLE_shortExact 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ ∃ (X_1 : DerivedCategory.{w, v, u} C) (Y : DerivedCategory.{w, v, u} C) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : X_1 ≅ Functor.obj Q K), K.IsStrictlyLE 0) (_ :
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyGE 1) (f : X_1 ⟶ X) (g : X ⟶ Y) (h :
    Y ⟶ Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) X_1),
    Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
      (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) (Triangle.mk f g h)
have refine : triangleOfSES h ≅
  Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
    (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
    (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
      Triangle.mor₃ (triangleOfSES h))
Tactic: refine ⟨Q.obj (K.truncLE 0), Q.obj (K.truncGE 1),
      ⟨_, Iso.refl _, inferInstance⟩, ⟨_, Iso.refl _, inferInstance⟩,
      Q.map (K.ιTruncLE 0) ≫ e₂.hom, e₂.inv ≫ Q.map (K.πTruncGE 1),
      inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by lia))) ≫ (triangleOfSES h).mor₃,
      isomorphic_distinguished _ (triangleOfSES_distinguished h) _ (Iso.symm ?_)⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ triangleOfSES h ≅
    Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
      (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
      (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
        Triangle.mor₃ (triangleOfSES h))
have refine_1 : Triangle.mor₁ (triangleOfSES h) ≫ e₂.hom =
  Iso.hom (Iso.refl (Triangle.obj₁ (triangleOfSES h))) ≫
    Triangle.mor₁
      (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
        (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
        (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
          Triangle.mor₃ (triangleOfSES h)))
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) e₂
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by lia)))) ?_ ?_ (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
refine_1 :
  Triangle.mor₁ (triangleOfSES h) ≫ e₂.hom =
    Iso.hom (Iso.refl (Triangle.obj₁ (triangleOfSES h))) ≫
      Triangle.mor₁
        (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
          (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
          (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
            Triangle.mor₃ (triangleOfSES h)))
⊢ triangleOfSES h ≅
    Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
      (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
      (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
        Triangle.mor₃ (triangleOfSES h))
have refine_2 : Eq.{w + 1} (α :=
  Triangle.obj₂ (triangleOfSES h) ⟶
    Triangle.obj₃
      (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
        (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
        (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
          Triangle.mor₃ (triangleOfSES h))))
  (Triangle.mor₂ (triangleOfSES h) ≫
    Iso.hom (asIso (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12))))
  (e₂.hom ≫
    Triangle.mor₂
      (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
        (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
        (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
          Triangle.mor₃ (triangleOfSES h))))
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) e₂
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by lia)))) ?_ ?_ (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Triangle.mor₁ (triangleOfSES h) ≫ e₂.hom =
    Iso.hom (Iso.refl (Triangle.obj₁ (triangleOfSES h))) ≫
      Triangle.mor₁
        (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
          (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
          (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
            Triangle.mor₃ (triangleOfSES h)))
have refine_1 : Eq (α := Functor.obj Q (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0)) ⟶ X)
  (CategoryTheory.Functor.map Q (HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE 0)) ≫ e₂.hom)
  (𝟙 (Functor.obj Q (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0))) ≫
    CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Eq (α := Functor.obj Q (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0)) ⟶ X)
    (CategoryTheory.Functor.map Q (HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE 0)) ≫ e₂.hom)
    (𝟙 (Functor.obj Q (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0))) ≫
      CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
have refine_1 : Eq (α := Functor.obj Q (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0)) ⟶ X)
  (CategoryTheory.Functor.map Q (HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE 0)) ≫ e₂.hom)
  (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Eq.{w + 1} (α :=
    Triangle.obj₂ (triangleOfSES h) ⟶
      Triangle.obj₃
        (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
          (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
          (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
            Triangle.mor₃ (triangleOfSES h))))
    (Triangle.mor₂ (triangleOfSES h) ≫
      Iso.hom (asIso (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12))))
    (e₂.hom ≫
      Triangle.mor₂
        (Triangle.mk (X := Functor.obj Q (K.truncLE 0)) (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)
          (e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
          (inv (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12)) ≫
            Triangle.mor₃ (triangleOfSES h))))
have refine_2 : CategoryTheory.Functor.map Q (K.shortComplexTruncLE 0).g ≫
    CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
  e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ CategoryTheory.Functor.map Q (K.shortComplexTruncLE 0).g ≫
      CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
    e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
have refine_2 : CategoryTheory.Functor.map Q ((K.shortComplexTruncLE 0).g ≫ K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
  e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
Tactic: rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE,
        Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
refine_2 :
  CategoryTheory.Functor.map Q ((K.shortComplexTruncLE 0).g ≫ K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
    e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
⊢ CategoryTheory.Functor.map Q (K.shortComplexTruncLE 0).g ≫
      CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
    e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
have refine_2₁ : Eq (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K) (Functor.obj Q (K.truncGE 1)))
  (CategoryTheory.Functor.map Q (K.πTruncGE 1)) (e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
Tactic: rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE,
        Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e₂ : Functor.obj Q K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
refine_2 :
  CategoryTheory.Functor.map Q ((K.shortComplexTruncLE 0).g ≫ K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
    e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
refine_2₁ :
  Eq (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K) (Functor.obj Q (K.truncGE 1)))
    (CategoryTheory.Functor.map Q (K.πTruncGE 1)) (e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1))
⊢ CategoryTheory.Functor.map Q (K.shortComplexTruncLE 0).g ≫
      CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
    e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
have refine_2₂ : Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K) (Functor.obj Q (K.truncGE 1)))
  (CategoryTheory.Functor.map Q (K.πTruncGE 1)) (CategoryTheory.Functor.map Q (K.πTruncGE 1))
Tactic: rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE,
        Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
⊢ X.IsGE n ↔ ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have mp : X.IsGE n → ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
mp : X.IsGE n → ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ X.IsGE n ↔ ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have mpr : (∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)) → X.IsGE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h : K.IsStrictlyGE n
i : ℤ
hi : i < n
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have mp : Functor.obj (homologyFunctor C i) X ≅ HomologicalComplex.homology K i
Tactic: apply ((K.exactAt_of_isGE n i hi).isZero_homology).of_iso