awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n a n' : ℤ
h : a + n' = n
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h_1 : K.IsStrictlyGE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x :
    Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) a) X ≅ Functor.obj Q K), K.IsStrictlyGE n'

Tactic:
⟨(shiftFunctor (CochainComplex C ℤ) a).obj K,
      (shiftFunctor (DerivedCategory C) a).mapIso e ≪≫ (Q.commShiftIso a).symm.app K,
      K.isStrictlyGE_shift n a n' h⟩

Premises used: CochainComplex.isStrictlyGE_shift, DerivedCategory, DerivedCategory.Q, CategoryTheory.shiftFunctor, Int, CochainComplex, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n a n' : ℤ
h : a + n' = n
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h_1 : K.IsStrictlyGE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x :
    Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) a) X ≅ Functor.obj Q K), K.IsStrictlyGE n'

Tactic:
exact ⟨(shiftFunctor (CochainComplex C ℤ) a).obj K,
      (shiftFunctor (DerivedCategory C) a).mapIso e ≪≫ (Q.commShiftIso a).symm.app K,
      K.isStrictlyGE_shift n a n' h⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
rw : (e₁.inv ≫ f) ≫ e₂.hom = 0
⊢ f = 0

Tactic:
rw [← cancel_epi e₁.inv, ← cancel_mono e₂.hom, comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
⊢ LT.lt (α := ℤ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
⊢ (e₁.inv ≫ f) ≫ e₂.hom = 0

Tactic:
apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE K L 0 1 (by simp)).elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : X ≅ Functor.obj Q K
h : K.IsStrictlyLE 0
⊢ LE.le (α := ℤ) 0 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : X ≅ Functor.obj Q K
h : K.IsStrictlyLE 0
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : X ≅ Functor.obj Q K), K.IsStrictlyLE 1

Tactic:
exact ⟨K, e, K.isStrictlyLE_of_le 0 1 (by lia)⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : X ≅ Functor.obj Q K
h : K.IsStrictlyGE 1
⊢ LE.le (α := ℤ) 0 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : X ≅ Functor.obj Q K
h : K.IsStrictlyGE 1
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : X ≅ Functor.obj Q K), K.IsStrictlyGE 0

Tactic:
exact ⟨K, e, K.isStrictlyGE_of_ge 0 1 (by lia)⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 ℤ), Nonempty.{w + 1} (Functor.obj Q K ≅ X)

Tactic:
⟨_, ⟨Q.objObjPreimageIso X⟩⟩

Premises used: DerivedCategory.Q, Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
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 _ _ ⋯ _ instPreadditive ⋯ _) (Triangle.mk f g h)
⊢ ∃ (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)

Tactic:
obtain ⟨K, ⟨e₂⟩⟩ : ∃ K, Nonempty (Q.obj K ≅ X) := ⟨_, ⟨Q.objObjPreimageIso X⟩⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
⊢ (K.shortComplexTruncLE 0).ShortExact

Tactic:
have h := K.shortComplexTruncLE_shortExact 0
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
⊢ HAdd.hAdd (α := ℤ) 0 1 = 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 :
  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))
⊢ ∃ (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)

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 ?_)⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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) ⟶
      Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (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) ≫
      CategoryTheory.Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
        (Iso.hom (Iso.refl (Triangle.obj₁ (triangleOfSES h)))))
    (Iso.hom (asIso (CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12))) ≫
      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:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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)))
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))))
⊢ 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 Triangle.isoMk _ _ (Iso.refl _) e₂
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 (by lia)))) ?_ ?_ (by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 :
  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)
⊢ 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:
dsimp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 :
  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)
⊢ 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:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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)
    (CategoryTheory.Functor.map Q (K.ιTruncLE 0) ≫ e₂.hom)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 ≫
      CategoryTheory.Functor.map Q (K.shortComplexTruncLEX₃ToTruncGE 0 1 t._proof_12) =
    e₂.hom ≫ e₂.inv ≫ CategoryTheory.Functor.map Q (K.πTruncGE 1)
⊢ 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:
dsimp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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))
refine_2₂ 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))
⊢ 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:
rw [← Q.map_comp, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE,
        Iso.hom_inv_id_assoc]

Premises used: DerivedCategory.Q, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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)
mpr : (∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)) → X.IsGE n
⊢ X.IsGE n ↔ ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
mp : Functor.obj (homologyFunctor C i) X ≅ HomologicalComplex.homology K i
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
apply ((K.exactAt_of_isGE n i hi).isZero_homology).of_iso

Premises used: CochainComplex.exactAt_of_isGE, CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.ExactAt.isZero_homology
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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
⊢ Functor.obj (homologyFunctor C i) X ≅ HomologicalComplex.homology K i

Tactic:
exact (homologyFunctor C i).mapIso e ≪≫ (homologyFunctorFactors C i).app K

Premises used: DerivedCategory.homologyFunctor, DerivedCategory.homologyFunctorFactors, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
rw : ∀ i < n, HomologicalComplex.ExactAt (Functor.objPreimage Q X) i
⊢ (Functor.objPreimage Q X).IsGE n

Tactic:
rw [CochainComplex.isGE_iff]

Premises used: CochainComplex.isGE_iff
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : i < n
rw : IsZero.{v, u} (HomologicalComplex.homology (Functor.objPreimage Q X) i)
⊢ HomologicalComplex.ExactAt (Functor.objPreimage Q X) i

Tactic:
rw [HomologicalComplex.exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : i < n
apply : HomologicalComplex.homology (Functor.objPreimage Q X) i ≅ Functor.obj (homologyFunctor C i) X
⊢ IsZero.{v, u} (HomologicalComplex.homology (Functor.objPreimage Q X) i)

Tactic:
apply (hX i hi).of_iso

Premises used: CategoryTheory.Limits.IsZero.of_iso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : i < n
⊢ HomologicalComplex.homology (Functor.objPreimage Q X) i ≅ Functor.obj (homologyFunctor C i) X

Tactic:
exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)

Premises used: DerivedCategory.Q, DerivedCategory.homologyFunctor, CategoryTheory.Functor.objObjPreimageIso, DerivedCategory.homologyFunctorFactors, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ (Functor.objPreimage Q X).IsGE n

Tactic:
have : (Q.objPreimage X).IsGE n := by
      rw [CochainComplex.isGE_iff]
      intro i hi
      rw [HomologicalComplex.exactAt_iff_isZero_homology]
      apply (hX i hi).of_iso
      exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
this : (Functor.objPreimage Q X).IsGE n
⊢ X.IsGE n

Tactic:
⟨(Q.objPreimage X).truncGE n, (Q.objObjPreimageIso X).symm ≪≫
      asIso (Q.map ((Q.objPreimage X).πTruncGE n)), inferInstance⟩

Premises used: DerivedCategory.Q, inferInstance, CategoryTheory.Functor.objPreimage, CategoryTheory.Functor.map, CochainComplex.truncGE, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Triangulated.TStructure.IsGE.mk, CategoryTheory.asIso, CochainComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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 : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
this : (Functor.objPreimage Q X).IsGE n
⊢ X.IsGE n

Tactic:
exact ⟨(Q.objPreimage X).truncGE n, (Q.objObjPreimageIso X).symm ≪≫
      asIso (Q.map ((Q.objPreimage X).πTruncGE n)), inferInstance⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
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.IsLE n → ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
mpr : (∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)) → X.IsLE n
⊢ X.IsLE n ↔ ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
constructor