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
X : DerivedCategory.{w, v, u} C
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h : K.IsStrictlyLE n
i : ℤ
hi : n < i
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_isLE n i hi).isZero_homology).of_iso

Premises used: CochainComplex.exactAt_of_isLE, 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.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ 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 < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
rw : ∀ (i : ℤ), n < i → HomologicalComplex.ExactAt (Functor.objPreimage Q X) i
⊢ (Functor.objPreimage Q X).IsLE n

Tactic:
rw [CochainComplex.isLE_iff]

Premises used: CochainComplex.isLE_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 < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : n < i
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 < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : n < i
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 < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : n < i
⊢ 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 < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ (Functor.objPreimage Q X).IsLE n

Tactic:
have : (Q.objPreimage X).IsLE n := by
      rw [CochainComplex.isLE_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 < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
this : (Functor.objPreimage Q X).IsLE n
⊢ X.IsLE n

Tactic:
⟨(Q.objPreimage X).truncLE n, (Q.objObjPreimageIso X).symm ≪≫
      (asIso (Q.map ((Q.objPreimage X).ιTruncLE n))).symm, inferInstance⟩

Premises used: CochainComplex.truncLE, DerivedCategory.Q, inferInstance, CochainComplex.ιTruncLE, CategoryTheory.Functor.objPreimage, CategoryTheory.Functor.map, CategoryTheory.Triangulated.TStructure.IsLE.mk, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm, 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
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
this : (Functor.objPreimage Q X).IsLE n
⊢ X.IsLE n

Tactic:
exact ⟨(Q.objPreimage X).truncLE n, (Q.objObjPreimageIso X).symm ≪≫
      (asIso (Q.map ((Q.objPreimage X).ιTruncLE n))).symm, 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 i : ℤ
hi : i < n
hX : X.IsGE n
⊢ ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
rw [isGE_iff] at hX

Premises used: DerivedCategory.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 i : ℤ
hi : i < n
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
hX i hi
-- 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 i : ℤ
hi : i < n
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
exact hX i hi
-- 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 i : ℤ
hi : n < i
hX : X.IsLE n
⊢ ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
rw [isLE_iff] at hX

Premises used: DerivedCategory.isLE_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 i : ℤ
hi : n < i
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
hX i hi
-- 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 i : ℤ
hi : n < i
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)

Tactic:
exact hX i hi
-- 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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ ∀ (i : ℤ),
    IsZero.{v, u} (Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Q (homologyFunctor C i)) K) ↔
      IsZero.{v, u} (Functor.obj (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) i) K)

Tactic:
have eq := fun i ↦ ((homologyFunctorFactors C i).app K).isZero_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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
eq :
  ∀ (i : ℤ),
    IsZero.{v, u} (Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C i) (Functor.obj Q K)) ↔
      IsZero.{v, u} (HomologicalComplex.homology K i)
⊢ IsGE.{w, v, u} (Functor.obj Q K) n ↔ K.IsGE n

Tactic:
simp only [isGE_iff, CochainComplex.isGE_iff,
    HomologicalComplex.exactAt_iff_isZero_homology, eq]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology, DerivedCategory.isGE_iff, 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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
eq :
  ∀ (i : ℤ),
    IsZero.{v, u} (Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C i) (Functor.obj Q K)) ↔
      IsZero.{v, u} (HomologicalComplex.homology K i)
⊢ IsLE.{w, v, u} (Functor.obj Q K) n ↔ K.IsLE n

Tactic:
simp only [isLE_iff, CochainComplex.isLE_iff,
    HomologicalComplex.exactAt_iff_isZero_homology, eq]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology, DerivedCategory.isLE_iff, CochainComplex.isLE_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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 rw : K.IsGE n
⊢ IsGE.{w, v, u} (Functor.obj Q K) n

Tactic:
rw [isGE_Q_obj_iff]

Premises used: DerivedCategory.isGE_Q_obj_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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : K.IsGE n
⊢ K.IsGE n

Tactic:
infer_instance
-- 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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 rw : K.IsLE n
⊢ IsLE.{w, v, u} (Functor.obj Q K) n

Tactic:
rw [isLE_Q_obj_iff]

Premises used: DerivedCategory.isLE_Q_obj_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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_3 : K.IsLE n
⊢ K.IsLE n

Tactic:
infer_instance
-- 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 : C
n : ℤ
e : Iso (C := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) X)
  (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) X)) :=
  Iso.app (singleFunctorIsoCompQ C n) X
⊢ IsGE.{w, v, u} (Functor.obj (singleFunctor C n) X) n

Tactic:
TStructure.t.isGE_of_iso e.symm n

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, DerivedCategory.TStructure.t, CategoryTheory.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 : C
n : ℤ
e : Iso (C := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) X)
  (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) X)) :=
  Iso.app (singleFunctorIsoCompQ C n) X
⊢ IsGE.{w, v, u} (Functor.obj (singleFunctor C n) X) n

Tactic:
exact TStructure.t.isGE_of_iso e.symm n

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, DerivedCategory.TStructure.t, CategoryTheory.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 : C
n : ℤ
e : Iso (C := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) X)
  (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) X)) :=
  Iso.app (singleFunctorIsoCompQ C n) X
⊢ IsLE.{w, v, u} (Functor.obj (singleFunctor C n) X) n

Tactic:
TStructure.t.isLE_of_iso e.symm n

Premises used: DerivedCategory.TStructure.t, CategoryTheory.Triangulated.TStructure.isLE_of_iso, CategoryTheory.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 : C
n : ℤ
e : Iso (C := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) X)
  (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) X)) :=
  Iso.app (singleFunctorIsoCompQ C n) X
⊢ IsLE.{w, v, u} (Functor.obj (singleFunctor C n) X) n

Tactic:
exact TStructure.t.isLE_of_iso e.symm n

Premises used: DerivedCategory.TStructure.t, CategoryTheory.Triangulated.TStructure.isLE_of_iso, CategoryTheory.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
n : ℤ
hX : X.IsLE n
obtain :
  ∀ (K : CochainComplex.{v, u, 0} C ℤ) (e : X ≅ Functor.obj Q K),
    K.IsStrictlyLE n →
      ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyLE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyLE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
obtain ⟨K, e, _⟩ := hX
-- 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.IsStrictlyLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyLE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
⟨K, inferInstance, ⟨e⟩⟩

Premises used: inferInstance, Nonempty.intro, 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
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h : K.IsStrictlyLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyLE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
exact ⟨K, inferInstance, ⟨e⟩⟩
-- 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 : X.IsGE n
obtain :
  ∀ (K : CochainComplex.{v, u, 0} C ℤ) (e : X ≅ Functor.obj Q K),
    K.IsStrictlyGE n →
      ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
obtain ⟨K, e, _⟩ := hX
-- 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
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
⟨K, inferInstance, ⟨e⟩⟩

Premises used: inferInstance, Nonempty.intro, 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
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h : K.IsStrictlyGE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
exact ⟨K, inferInstance, ⟨e⟩⟩
-- 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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
obtain :
  ∀ (K : CochainComplex.{v, u, 0} C ℤ) (hK : K.IsStrictlyLE b) (e : X ≅ Functor.obj Q K),
    ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
      Nonempty.{w + 1} (X ≅ Functor.obj Q K)
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
    Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
obtain ⟨K, hK, ⟨e⟩⟩ := X.exists_iso_Q_obj_of_isLE b

Premises used: DerivedCategory.exists_iso_Q_obj_of_isLE
-- 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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
rw : IsGE.{w, v, u} (Functor.obj Q K) a
⊢ K.IsGE a

Tactic:
rw [← isGE_Q_obj_iff]

Premises used: DerivedCategory.isGE_Q_obj_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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
⊢ IsGE.{w, v, u} (Functor.obj Q K) a

Tactic:
TStructure.t.isGE_of_iso e a

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, DerivedCategory.TStructure.t
-- 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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
⊢ IsGE.{w, v, u} (Functor.obj Q K) a

Tactic:
exact TStructure.t.isGE_of_iso e a

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_iso, DerivedCategory.TStructure.t
-- 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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
⊢ K.IsGE a

Tactic:
have : K.IsGE a := by
    rw [← isGE_Q_obj_iff]
    exact TStructure.t.isGE_of_iso e a
-- 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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
this : K.IsGE a
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
    Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
⟨K.truncGE a, inferInstance, inferInstance, ⟨e ≪≫ asIso (Q.map (K.πTruncGE a))⟩⟩

Premises used: DerivedCategory.Q, inferInstance, Nonempty.intro, CategoryTheory.Functor.map, CochainComplex.truncGE, CategoryTheory.Iso.trans, Exists.intro, 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
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
this : K.IsGE a
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
    Nonempty.{w + 1} (X ≅ Functor.obj Q K)

Tactic:
exact ⟨K.truncGE a, inferInstance, inferInstance, ⟨e ≪≫ asIso (Q.map (K.πTruncGE a))⟩⟩
-- 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 : ℤ
inst_3 : X.IsGE n
inst_4 : X.IsLE n
obtain :
  ∀ (K : CochainComplex.{v, u, 0} C ℤ),
    K.IsStrictlyGE n →
      K.IsStrictlyLE n →
        ∀ (e : X ≅ Functor.obj Q K), ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)
⊢ ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)

Tactic:
obtain ⟨K, _, _, ⟨e⟩⟩ := exists_iso_Q_obj_of_isGE_of_isLE X n n

Premises used: DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE
-- 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 : ℤ
inst_3 : X.IsGE n
inst_4 : X.IsLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyGE n
w_1 : K.IsStrictlyLE n
e : X ≅ Functor.obj Q K
obtain :
  ∀ (Y : C) (e' : K ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) Y),
    ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)
⊢ ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)

Tactic:
obtain ⟨Y, ⟨e'⟩⟩ := CochainComplex.exists_iso_single K n

Premises used: CochainComplex.exists_iso_single
-- 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 : ℤ
inst_3 : X.IsGE n
inst_4 : X.IsLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyGE n
w_1 : K.IsStrictlyLE n
e : X ≅ Functor.obj Q K
Y : C
e' : K ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) Y
⊢ ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)

Tactic:
⟨Y, ⟨e ≪≫ Q.mapIso e'⟩⟩

Premises used: DerivedCategory.Q, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, 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 : ℤ
inst_3 : X.IsGE n
inst_4 : X.IsLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyGE n
w_1 : K.IsStrictlyLE n
e : X ≅ Functor.obj Q K
Y : C
e' : K ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) Y
⊢ ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)

Tactic:
exact ⟨Y, ⟨e ≪≫ Q.mapIso e'⟩⟩
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i : β
⊢ X.objEqToHom ⋯ = 𝟙 (X.obj i)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
refl :
  Eq.{u_1 + 1} (α := β) ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
    ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
⊢ Eq.{u_1 + 1} (α := β) ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
    ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) y)

Tactic:
cases h
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ Eq.{u_1 + 1} (α := β) ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
    ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)

Tactic:
rfl