awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
X Y : C
n : ℤ
hn : 0 ≤ n
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))

Tactic:
(small_congr ((shiftFunctorZero _ ℤ).app
      ((singleFunctor C 0).obj X)).homFromEquiv).1 (h X Y 0 n)

Premises used: small_congr, CategoryTheory.shiftFunctorZero, Int, Iff.mp, CategoryTheory.Iso.app, OfNat.ofNat, DerivedCategory.singleFunctor, CategoryTheory.Iso.homFromEquiv, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
X Y : C
n : ℤ
hn : 0 ≤ n
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))

Tactic:
exact (small_congr ((shiftFunctorZero _ ℤ).app
      ((singleFunctor C 0).obj X)).homFromEquiv).1 (h X Y 0 n)

Premises used: small_congr, CategoryTheory.shiftFunctorZero, Int, Iff.mp, CategoryTheory.Iso.app, OfNat.ofNat, DerivedCategory.singleFunctor, CategoryTheory.Iso.homFromEquiv, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
mpr :
  ∀ (hab : a ≤ b),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
mpr₁ :
  ∀ (hab : b < a),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))

Tactic:
obtain hab | hab := le_or_gt a b

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : a ≤ b
⊢ 0 ≤ b - a

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : a ≤ b
mpr :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) (b - a)) (Functor.obj (singleFunctor C 0) Y)) ≃
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))

Tactic:
refine (small_congr ?_).1 (h X Y (b - a) (by simpa))

Premises used: small_congr, HSub.hSub, Iff.mp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : a ≤ b
⊢ Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) (b - a)) (Functor.obj (singleFunctor C 0) Y)) ≃
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))

Tactic:
exact (Functor.FullyFaithful.ofFullyFaithful
        (shiftFunctor _ a)).homEquiv.trans
        ((shiftFunctorAdd' _ _ _ _ (Int.sub_add_cancel b a)).symm.app _).homToEquiv

Premises used: CategoryTheory.Iso.homToEquiv, Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.shiftFunctor, CategoryTheory.shiftFunctorAdd', Int.sub_add_cancel, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
mpr :
  Subsingleton.{w' + 1}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))

Tactic:
suffices Subsingleton ((Q.obj ((CochainComplex.singleFunctor C 0).obj X))⟦a⟧ ⟶
          (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))⟦b⟧) from inferInstance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
mpr :
  ∀
    (a_1 b_1 :
      Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
          (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))),
    a_1 = b_1
⊢ Subsingleton.{w' + 1}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
      (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y))))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
mpr :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) X))
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      x ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      y ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
⊢ x = y

Tactic:
rw [← cancel_mono ((Q.commShiftIso b).inv.app _),
        ← cancel_epi ((Q.commShiftIso a).hom.app _)]

Premises used: DerivedCategory.Q, CategoryTheory.cancel_mono, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
⊢ a + -a = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
⊢ CochainComplex.IsStrictlyLE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (-a)

Tactic:
have : (((CochainComplex.singleFunctor C 0).obj X)⟦a⟧).IsStrictlyLE (-a) :=
        CochainComplex.isStrictlyLE_shift _ 0 _ _ (by lia)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
this :
  CochainComplex.IsStrictlyLE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (-a)
⊢ b + -b = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
this :
  CochainComplex.IsStrictlyLE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (-a)
⊢ CochainComplex.IsStrictlyGE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (-b)

Tactic:
have : (((CochainComplex.singleFunctor C 0).obj Y)⟦b⟧).IsStrictlyGE (-b) :=
        CochainComplex.isStrictlyGE_shift _ 0 _ _ (by lia)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
this_1 :
  CochainComplex.IsStrictlyLE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (-a)
this :
  CochainComplex.IsStrictlyGE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (-b)
⊢ -a < -b

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w', v, u} C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'}
        (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
X Y : C
a b : ℤ
hab : b < a
x y :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C)
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
this_1 :
  CochainComplex.IsStrictlyLE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (-a)
this :
  CochainComplex.IsStrictlyGE.{v, u}
    (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (-b)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory.{w', v, u} C)
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) X))
      (Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) b ⋙ Q)
        (Functor.obj (CochainComplex.singleFunctor C 0) Y)))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      x ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso Q a)) (Functor.obj (CochainComplex.singleFunctor C 0) X) ≫
      y ≫ NatTrans.app (Iso.inv (Functor.commShiftIso Q b)) (Functor.obj (CochainComplex.singleFunctor C 0) Y))

Tactic:
apply (subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE _ _ (-a) (-b) (by
        lia)).elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
rw :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w}
        (Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))
⊢ HasExt.{w, v, u} C

Tactic:
rw [hasExt_iff.{w}]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
⊢ ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w}
        (Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) n) (Functor.obj (singleFunctor C 0) Y)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_2 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasExt C

Tactic:
hasExt_of_hasDerivedCategory _

Premises used: CategoryTheory.hasExt_of_hasDerivedCategory
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_2 : Abelian.{v, u} C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasExt C

Tactic:
exact hasExt_of_hasDerivedCategory _

Premises used: CategoryTheory.hasExt_of_hasDerivedCategory
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
a b : ℤ
inst_3 : HasDerivedCategory.{w', v, u} C
⊢ ∀ (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a) (Functor.obj (singleFunctor C 0) X))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b) (Functor.obj (singleFunctor C 0) Y)))

Tactic:
have (a b : ℤ) :
      Small.{w} (((singleFunctor C 0).obj X)⟦a⟧ ⟶ ((singleFunctor C 0).obj Y)⟦b⟧) :=
    (hasSmallLocalizedShiftedHom_iff.{w}
      (W := (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))) (M := ℤ)
      (X := (CochainComplex.singleFunctor C 0).obj X)
      (Y := (CochainComplex.singleFunctor C 0).obj Y) Q).1 inferInstance a b
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
a b : ℤ
inst_3 : HasDerivedCategory.{w', v, u} C
this :
  ∀ (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a) (Functor.obj (singleFunctor C 0) X))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b) (Functor.obj (singleFunctor C 0) Y)))
φ :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C a) X) (Functor.obj (singleFunctor C b) Y)
⊢ -a + a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
a b : ℤ
inst_3 : HasDerivedCategory.{w', v, u} C
this :
  ∀ (a b : ℤ),
    Small.{w, w'}
      (Quiver.Hom (V := DerivedCategory.{w', v, u} C)
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) a) (Functor.obj (singleFunctor C 0) X))
        (Functor.obj (shiftFunctor (DerivedCategory.{w', v, u} C) b) (Functor.obj (singleFunctor C 0) Y)))
φ :
  Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C a) X) (Functor.obj (singleFunctor C b) Y)
⊢ -b + b = 0

Tactic:
simp