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 : HasExt.{w, v, u} C
X Y Z : C
n : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
β₁ β₂ : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (α.comp (β₁ + β₂) h).hom (α.comp β₁ h + α.comp β₂ h).hom

Tactic:
simp [this, add_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.add_hom'
-- 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 Z : C
n : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
β : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    ((-α).comp β h).hom (-α.comp β h).hom
⊢ (-α).comp β h = -α.comp β h

Tactic:
ext
-- 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 Z : C
n : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
β : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    ((-α).comp β h).hom (-α.comp β h).hom

Tactic:
simp [this, neg_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.neg_hom'
-- 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 Z : C
n : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
β : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (α.comp (-β) h).hom (-α.comp β h).hom
⊢ α.comp (-β) h = -α.comp β h

Tactic:
ext
-- 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 Z : C
n : ℕ
α : Ext.{w, v, u} X Y n
m : ℕ
β : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (α.comp (-β) h).hom (-α.comp β h).hom

Tactic:
simp [this, neg_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.neg_hom'
-- 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 Z : C
n m : ℕ
β : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (hom (comp 0 β h)) (hom 0)
⊢ Eq (α := Ext.{w, v, u} X Z p) (comp 0 β h) 0

Tactic:
ext
-- 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 Z : C
n m : ℕ
β : Ext.{w, v, u} Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (hom (comp 0 β h)) (hom 0)

Tactic:
simp [this, zero_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.zero_hom'
-- 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
n : ℕ
α : Ext.{w, v, u} X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (hom (α.comp 0 h)) (hom 0)
⊢ Eq (α := Ext.{w, v, u} X Z p) (α.comp 0 h) 0

Tactic:
ext
-- 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
n : ℕ
α : Ext.{w, v, u} X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Z)
      (↑p : ℤ))
    (hom (α.comp 0 h)) (hom 0)

Tactic:
simp [this, zero_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.zero_hom'
-- 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
n : ℕ
α : Ext.{w, v, u} X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑n : ℤ))
    (comp (mk₀ (𝟙 X)) α ⋯).hom α.hom
⊢ comp (mk₀ (𝟙 X)) α ⋯ = α

Tactic:
ext
-- 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
n : ℕ
α : Ext.{w, v, u} X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑n : ℤ))
    (comp (mk₀ (𝟙 X)) α ⋯).hom α.hom

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
n : ℕ
α : Ext.{w, v, u} X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑n : ℤ))
    (α.comp (mk₀ (𝟙 Y)) ⋯).hom α.hom
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α

Tactic:
ext
-- 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
n : ℕ
α : Ext.{w, v, u} X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑n : ℤ))
    (α.comp (mk₀ (𝟙 Y)) ⋯).hom α.hom

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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (hom (mk₀ 0)) (hom 0)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0) (mk₀ 0) 0

Tactic:
ext
-- 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
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (hom (mk₀ 0)) (hom 0)

Tactic:
simp [zero_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.zero_hom'
-- 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
f g : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (hom (mk₀ (f + g))) (HAdd.hAdd (α := Ext.{w, v, u} X Y 0) (mk₀ f) (mk₀ g)).hom
⊢ mk₀ (f + g) = HAdd.hAdd (α := Ext.{w, v, u} X Y 0) (mk₀ f) (mk₀ g)

Tactic:
ext
-- 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
f g : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (hom (mk₀ (f + g))) (HAdd.hAdd (α := Ext.{w, v, u} X Y 0) (mk₀ f) (mk₀ g)).hom

Tactic:
simp [add_hom', ShiftedHom.mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀, _private.0.CategoryTheory.Abelian.Ext.add_hom'
-- 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 Z T : C
n : ℕ
x y : Ext.{w, v, u} X Y 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv₀ : (a : X ⟶ Y) → Ext X Y 0) (Equiv.toFun homEquiv₀ (x + y)) : Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv₀ : (a : X ⟶ Y) → Ext X Y 0) (Equiv.toFun homEquiv₀ x + Equiv.toFun homEquiv₀ y) :
      Ext.{w, v, u} X Y 0)

Tactic:
simp [mk₀_add]

Premises used: CategoryTheory.Abelian.Ext.mk₀_add
-- 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
f : Ext.{w, v, u} X Y 0
⊢ mk₀ ((addEquiv₀ : (a : Ext X Y 0) → X ⟶ Y) f) = f

Tactic:
addEquiv₀.left_inv f

Premises used: CategoryTheory.Localization.SmallHom.mk, CategoryTheory.Localization.SmallShiftedHom.mk₀, AddEquiv.toEquiv, CategoryTheory.Abelian.Ext.addEquiv₀, CategoryTheory.Localization.SmallShiftedHom.mk, CategoryTheory.Abelian.Ext.mk₀, Equiv.left_inv
-- 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
M N : C
f : M ⟶ N
⊢ Eq.{w + 1} (α := Ext.{w, v, u} M N 0) (mk₀ f) 0 ↔ f = 0

Tactic:
Ext.addEquiv₀.symm.map_eq_zero_iff (x := f)

Premises used: CategoryTheory.Localization.SmallHom.mk, AddEquiv.map_eq_zero_iff, CategoryTheory.Localization.SmallShiftedHom.mk₀, CategoryTheory.Localization.SmallShiftedHom.mk, CategoryTheory.Abelian.Ext.mk₀
-- 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
f : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (hom (mk₀ (-f))) (hom (-mk₀ f))
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0) (mk₀ (-f)) (-mk₀ f)

Tactic:
ext
-- 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
f : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (hom (mk₀ (-f))) (hom (-mk₀ f))

Tactic:
simp [neg_hom']

Premises used: _private.0.CategoryTheory.Abelian.Ext.neg_hom'
-- 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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
h₁ : comp (mk₀ biprod.inl) α ⋯ = comp (mk₀ biprod.inl) β ⋯
h₂ : comp (mk₀ biprod.inr) α ⋯ = comp (mk₀ biprod.inr) β ⋯
this : HasDerivedCategory C := HasDerivedCategory.standard C
rw :
  ∀
    (h₂ :
      Eq (α :=
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        (comp (mk₀ biprod.inr) α ⋯).hom (comp (mk₀ biprod.inr) β ⋯).hom)
    (h₁ :
      Eq (α :=
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        (comp (mk₀ biprod.inl) α ⋯).hom (comp (mk₀ biprod.inl) β ⋯).hom),
    Eq (α :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) (biprod.{v, u} X₁ X₂))
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      α.hom β.hom
⊢ α = β

Tactic:
rw [Ext.ext_iff] at h₁ h₂ ⊢

Premises used: CategoryTheory.Abelian.Ext.ext_iff
-- 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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₂ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (comp (mk₀ biprod.inr) α ⋯).hom (comp (mk₀ biprod.inr) β ⋯).hom
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (comp (mk₀ biprod.inl) α ⋯).hom (comp (mk₀ biprod.inl) β ⋯).hom
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inl ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inl ≫ β.hom)

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.ShiftedHom.mk₀_comp, CategoryTheory.Abelian.Ext.comp_hom
-- 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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₂ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (comp (mk₀ biprod.inr) α ⋯).hom (comp (mk₀ biprod.inr) β ⋯).hom
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (comp (mk₀ biprod.inl) α ⋯).hom (comp (mk₀ biprod.inl) β ⋯).hom
h₃ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inl ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inl ≫ β.hom)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inr ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inr ≫ β.hom)

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.ShiftedHom.mk₀_comp, CategoryTheory.Abelian.Ext.comp_hom
-- 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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inl ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inl ≫ β.hom)
h₂ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inr ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inr ≫ β.hom)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj (pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
        { as := WalkingPair.left : Discrete WalkingPair })
      (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) (↑n : ℤ)) (Functor.obj (singleFunctor C 0) Y)))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
            (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl
        (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
      α.hom)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
            (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl
        (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
      β.hom)

Tactic:
assumption
-- 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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext.{w, v, u} (biprod.{v, u} X₁ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₁)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inl ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inl ≫ β.hom)
h₂ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X₂)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (Functor.map (singleFunctor C 0) biprod.inr ≫ α.hom) (Functor.map (singleFunctor C 0) biprod.inr ≫ β.hom)
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj (pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
        { as := WalkingPair.right : Discrete WalkingPair })
      (Functor.obj (shiftFunctor (DerivedCategory C) (A := ℤ) (↑n : ℤ)) (Functor.obj (singleFunctor C 0) Y)))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
            (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr
        (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
      α.hom)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (Functor.obj (singleFunctor C 0) X₁) (Functor.obj (singleFunctor C 0) X₂))
            (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂)))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr
        (BinaryBicone.toCocone (Functor.mapBinaryBicone (singleFunctor C 0) (BinaryBiproduct.bicone X₁ X₂))))
      β.hom)

Tactic:
assumption
-- 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
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
β : Ext.{w, v, u} 0 Y n := 0
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) 0)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    β.hom 0

Tactic:
apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Functor.map_isZero, CategoryTheory.Limits.IsZero.eq_of_src
-- 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
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
β : Ext.{w, v, u} 0 Y n := 0
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) 0)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    β.hom 0

Tactic:
have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src
-- 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
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
β : Ext.{w, v, u} 0 Y n := 0
hβ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) 0)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    β.hom 0
⊢ Eq (α := Ext.{w, v, u} X Y n) 0 (comp 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
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
β : Ext.{w, v, u} 0 Y n := 0
hβ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) 0)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    β.hom 0
⊢ Eq (α := Ext.{w, v, u} X Y n) 0 (comp 0 β ⋯)

Tactic:
have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by 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
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
β : Ext.{w, v, u} 0 Y n := 0
hβ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) 0)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    β.hom 0
this : Eq (α := Ext.{w, v, u} X Y n) 0 (comp 0 β ⋯)
rw :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (hom (comp 0 β ⋯)) 0
rw₁ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (hom.{w', w, v, u} 0) β.hom ⋯) 0
rw₂ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (Y := Functor.obj (singleFunctor C 0) 0) (hom.{w', w, v, u} 0) 0 ⋯) 0
rw₃ rw₄ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    0 0
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (hom.{w', w, v, u} 0) 0

Tactic:
rw [this, comp_hom, hβ, ShiftedHom.comp_zero]

Premises used: CategoryTheory.ShiftedHom.comp_zero, CategoryTheory.Abelian.Ext.comp_hom
-- 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
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
⊢ α + β = comp (mk₀ (biprod.lift (𝟙 X) (𝟙 X))) (α' + β') ⋯

Tactic:
simp [α', β']