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 : 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)
h :
  Eq.{w' + 1} (α :=
    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)))
    ((fun
          (φ :
            Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C a) X)
              (Functor.obj (singleFunctor C b) Y)) ↦
        NatTrans.app (Iso.hom (SingleFunctors.shiftIso (singleFunctors C) (-a) a 0 ⋯)) X ≫
          φ ≫ NatTrans.app (Iso.inv (SingleFunctors.shiftIso (singleFunctors C) (-b) b 0 ⋯)) Y)
      φ₁)
    ((fun
          (φ :
            Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C a) X)
              (Functor.obj (singleFunctor C b) Y)) ↦
        NatTrans.app (Iso.hom (SingleFunctors.shiftIso (singleFunctors C) (-a) a 0 ⋯)) X ≫
          φ ≫ NatTrans.app (Iso.inv (SingleFunctors.shiftIso (singleFunctors C) (-b) b 0 ⋯)) Y)
      φ₂)
⊢ φ₁ = φ₂

Tactic:
simpa using h
-- 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)))
⊢ Small.{w, w'}
    (Quiver.Hom (V := DerivedCategory.{w', v, u} C) (Functor.obj (singleFunctor C a) X)
      (Functor.obj (singleFunctor C b) Y))

Tactic:
exact small_of_injective
    (β := ((singleFunctor C 0).obj X)⟦-a⟧ ⟶ ((singleFunctor C 0).obj Y)⟦-b⟧)
    (f := fun φ ↦
      ((singleFunctors C).shiftIso (-a) a 0 (by simp)).hom.app X ≫ φ ≫
        ((singleFunctors C).shiftIso (-b) b 0 (by simp)).inv.app Y)
    (fun φ₁ φ₂ h ↦ by simpa using h)

Premises used: small_of_injective
-- 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
a b : ℕ
α : Ext.{w, v, u} X Y a
β : Ext.{w, v, u} Y Z b
c : ℕ
h : a + b = c
⊢ HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑c : ℤ)

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 : HasExt.{w, v, u} C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z a₂
γ : Ext.{w, v, u} Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁₂ + a₃ = a

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 : HasExt.{w, v, u} C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z a₂
γ : Ext.{w, v, u} Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁ + a₂₃ = a

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 : HasExt.{w, v, u} C
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z a₂
γ : Ext.{w, v, u} Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ HAdd.hAdd (α := ℤ) (↑a₃ : ℤ) (↑a₂ : ℤ) + (↑a₁ : ℤ) = (↑a : ℤ)

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 : HasExt.{w, v, u} C
X Y Z T : C
a₁ a₃ a₁₃ : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z 0
γ : Ext.{w, v, u} Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
h : a₁ + 0 + a₃ = a₁₃
⊢ (α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃

Tactic:
apply comp_assoc

Premises used: CategoryTheory.Abelian.Ext.comp_assoc
-- 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
a₁ a₃ a₁₃ : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z 0
γ : Ext.{w, v, u} Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ a₁ + 0 + a₃ = a₁₃

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 : HasExt.{w, v, u} C
X Y Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z a₂
γ : Ext.{w, v, u} Z T 0
h₁₂ : a₁ + a₂ = a₁₂
h : a₁ + a₂ + 0 = a₁₂
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂

Tactic:
apply comp_assoc

Premises used: CategoryTheory.Abelian.Ext.comp_assoc
-- 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
a₁ a₂ a₁₂ : ℕ
α : Ext.{w, v, u} X Y a₁
β : Ext.{w, v, u} Y Z a₂
γ : Ext.{w, v, u} Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ a₁ + a₂ + 0 = a₁₂

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 : HasExt.{w, v, u} C
X Y Z T : C
inst_3 : HasDerivedCategory.{w', v, u} C
a b : ℕ
α : Ext.{w, v, u} X Y a
β : Ext.{w, v, u} Y Z b
c : ℕ
h : a + b = c
⊢ HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ) = (↑c : ℤ)

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 : HasExt.{w, v, u} C
X Y Z : C
inst_3 : HasDerivedCategory.{w', v, u} C
a b : ℕ
α : Ext.{w, v, u} X Y a
β : Ext.{w, v, u} Y Z b
c : ℕ
h : a + b = c
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Z) (↑c : ℤ))
    (α.comp β h).hom (ShiftedHom.comp α.hom β.hom ⋯)

Tactic:
apply SmallShiftedHom.equiv_comp

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_comp
-- 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
inst_3 : HasDerivedCategory.{w', v, u} C
n : ℕ
α β : Ext.{w, v, u} X Y n
h :
  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 β.hom
⊢ α = β

Tactic:
homEquiv.injective h

Premises used: CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective
-- 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
f : X ⟶ Y
⊢ Eq (α := ℤ) (↑0 : ℤ) 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 Z T : C
inst_3 : HasDerivedCategory.{w', v, u} C
f : X ⟶ Y
⊢ Eq (α := ℤ) (↑0 : ℤ) 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
inst_3 : HasDerivedCategory.{w', v, u} C
f : X ⟶ Y
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
    (hom.{w', w, v, u} (mk₀ f)) (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1 (Functor.map (singleFunctor C 0) f))

Tactic:
apply SmallShiftedHom.equiv_mk₀

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

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 Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext.{w, v, u} Z T n
h : HAdd.hAdd (α := ℕ) 0 0 + n = n
⊢ comp (mk₀ f) (comp (mk₀ g) α ⋯) ⋯ = comp (mk₀ (f ≫ g)) α ⋯

Tactic:
rw [← mk₀_comp_mk₀, comp_assoc]

Premises used: CategoryTheory.Abelian.Ext.comp_assoc, CategoryTheory.Abelian.Ext.mk₀_comp_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 Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext.{w, v, u} Z T n
⊢ HAdd.hAdd (α := ℕ) 0 0 + n = n

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 : HasExt.{w, v, u} C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
have :
  ∀ (h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)),
    Function.Bijective.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀
⊢ Function.Bijective.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀

Tactic:
have h : (singleFunctor C 0).FullyFaithful := 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 : HasExt.{w, v, u} C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
⊢ Eq (α := ℤ) (↑0 : ℤ) 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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
h₁ : ∀ (f : X ⟶ Y), e.toFun f = mk₀ f
⊢ e.toFun = mk₀

Tactic:
ext f : 1
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
h₁ :
  Eq.{w + 1} (α := Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
        (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f)) :
      Ext.{w, v, u} X Y 0)
    (mk₀ f : Ext.{w, v, u} X Y 0)
⊢ e.toFun f = mk₀ f

Tactic:
dsimp [e]
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
          (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f))) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        (mk₀ f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0)
    ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
        (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f)) :
      Ext.{w, v, u} X Y 0)
    (mk₀ f : Ext.{w, v, u} X Y 0)

Tactic:
apply homEquiv.injective

Premises used: CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ)) (mk₀ f))
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        ((Equiv.symm homEquiv : (a : ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) 0) → Ext X Y 0)
          (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f))) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        (mk₀ f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))

Tactic:
apply (Equiv.apply_symm_apply _ _).trans

Premises used: Equiv.apply_symm_apply, Eq.trans
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
h₁ :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        (mk₀ f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
    (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) 0)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ)) (mk₀ f))

Tactic:
symm
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
f : X ⟶ Y
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑0 : ℤ))
    ((homEquiv : (a : Ext X Y 0) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑0 : ℤ))
        (mk₀ f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑0 : ℤ))
    (ShiftedHom.mk₀ 0 ⋯ (Functor.map (singleFunctor C 0) f) :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) 0)

Tactic:
apply SmallShiftedHom.equiv_mk₀

Premises used: CategoryTheory.Localization.SmallShiftedHom.equiv_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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
⊢ e.toFun = mk₀

Tactic:
have he : e.toFun = mk₀ := by
    ext f : 1
    dsimp [e]
    apply homEquiv.injective
    apply (Equiv.apply_symm_apply _ _).trans
    symm
    apply SmallShiftedHom.equiv_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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
he : e.toFun = mk₀
rw : Function.Bijective e.toFun
⊢ Function.Bijective.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀

Tactic:
rw [← he]
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
he : e.toFun = mk₀
⊢ Function.Bijective e.toFun

Tactic:
e.bijective

Premises used: Equiv.bijective
-- 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 : Functor.FullyFaithful (D := DerivedCategory C) (singleFunctor C 0)
e : Equiv.{v + 1, w + 1} (X ⟶ Y) (Ext.{w, v, u} X Y 0) :=
  Equiv.trans (Equiv.trans h.homEquiv (ShiftedHom.homEquiv (↑0 : ℤ) ⋯)) (Equiv.symm homEquiv)
he : e.toFun = mk₀
⊢ Function.Bijective e.toFun

Tactic:
exact e.bijective

Premises used: Equiv.bijective
-- 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₀ ((homEquiv₀ : (a : Ext X Y 0) → X ⟶ Y) f) = f

Tactic:
homEquiv₀.left_inv f

Premises used: CategoryTheory.Localization.SmallHom.mk, CategoryTheory.Localization.SmallShiftedHom.mk₀, CategoryTheory.Abelian.Ext.homEquiv₀, 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
X Y : C
n : ℕ
α β : Ext.{w, v, u} X Y n
⊢ (α + β).hom' = α.hom' + β.hom'

Tactic:
letI := HasDerivedCategory.standard C
  homEquiv.symm.injective (Equiv.symm_apply_apply _ _)

Premises used: Equiv.symm_apply_apply, HAdd.hAdd, CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective, Equiv.symm
-- 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
⊢ (-α).hom' = -α.hom'

Tactic:
letI := HasDerivedCategory.standard C
  homEquiv.symm.injective (Equiv.symm_apply_apply _ _)

Premises used: Equiv.symm_apply_apply, CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective, Equiv.symm, Neg.neg
-- 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 : ℕ
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
      (↑n : ℤ))
    (hom'.{w, v, u} 0) 0

Tactic:
letI := HasDerivedCategory.standard C
  homEquiv.symm.injective (Equiv.symm_apply_apply _ _)

Premises used: Equiv.symm_apply_apply, CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective, Equiv.symm, OfNat.ofNat
-- 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 + α₂.comp β h).hom
⊢ (α₁ + α₂).comp β h = α₁.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 + α₂.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 + α.comp β₂ h).hom
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
ext