awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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 : ℤ))
    (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))
have 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 sorry (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: symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
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)
⊢ Function.Bijective.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀
have he : 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₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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.{v + 1, w + 1} (α := X ⟶ Y) (β := Ext.{w, v, u} X Y 0) mk₀
have rw : Function.Bijective e.toFun
Tactic: rw [← he]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ (-α).comp β h = -α.comp β h
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ α.comp (-β) h = -α.comp β h
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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 (α := Ext.{w, v, u} X Z p) (comp 0 β h) 0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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 (α := Ext.{w, v, u} X Z p) (α.comp 0 h) 0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ comp (mk₀ (𝟙 X)) α ⋯ = α
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
    (↑n : ℤ))
  (comp (mk₀ (𝟙 X)) α sorry).hom α.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) Y)
    (↑n : ℤ))
  (α.comp (mk₀ (𝟙 Y)) sorry).hom α.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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.{w + 1} (α := Ext.{w, v, u} X Y 0) (mk₀ 0) 0
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ mk₀ (f + g) = HAdd.hAdd (α := Ext.{w, v, u} X Y 0) (mk₀ f) (mk₀ g)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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.{w + 1} (α := Ext.{w, v, u} X Y 0) (mk₀ (-f)) (-mk₀ f)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ α = β
have 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) α sorry).hom (comp (mk₀ biprod.inr) β sorry).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) α sorry).hom (comp (mk₀ biprod.inl) β sorry).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₂ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
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) (biprod.{v, u} X₁ X₂))
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    α.hom β.hom
have 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)
Tactic: simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂
Cleared hypotheses: h₂, h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
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) (biprod.{v, u} X₁ X₂))
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    α.hom β.hom
have 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)
Tactic: simp only [comp_hom, mk₀_hom, ShiftedHom.mk₀_comp] at h₁ h₂
Cleared hypotheses: h₂, h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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 (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) (biprod.{v, u} X₁ X₂))
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    α.hom β.hom
have h₃ : 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: apply BinaryCofan.IsColimit.hom_ext
    (isBinaryBilimitOfPreserves (singleFunctor C 0)
      (BinaryBiproduct.isBilimit X₁ X₂)).isColimit
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
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) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (hom.{w', w, v, u} 0) 0
have 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
Tactic: have hβ : β.hom = 0 := by apply (Functor.map_isZero _ (isZero_zero C)).eq_of_src
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
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.{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
have this : Eq (α := Ext.{w, v, u} X Y n) 0 (comp 0 β sorry)
Tactic: have : (0 : Ext X Y n) = (0 : Ext X 0 0).comp β (zero_add n) := by simp [β]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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 β ⋯)
⊢ 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
have 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 β sorry)) 0
Tactic: rw [this, comp_hom, hβ, ShiftedHom.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ 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
have 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 sorry) 0
Tactic: rw [this, comp_hom, hβ, ShiftedHom.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ 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
have 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 sorry) 0
Tactic: rw [this, comp_hom, hβ, ShiftedHom.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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
⊢ 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
have 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
Tactic: rw [this, comp_hom, hβ, ShiftedHom.comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (hypothesis)
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) β ⋯
⊢ (α + β).hom =
    HAdd.hAdd (α :=
      ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
      α.hom β.hom
have eq₁ : α + β = comp (mk₀ (biprod.lift (𝟙 X) (𝟙 X))) (α' + β') sorry
Tactic: have eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') (zero_add n) := by
    simp [α', β']
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic (goal)
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) β ⋯
eq₁ : α + β = comp (mk₀ (biprod.lift (𝟙 X) (𝟙 X))) (α' + β') ⋯
⊢ α' + β' =
    (Equiv.symm homEquiv :
        (a : ShiftedHom ((singleFunctor C 0).obj (X ⊞ X)) ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext (X ⊞ X) Y n)
      (HAdd.hAdd (α :=
        ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        α'.hom β'.hom)
have h₁ : comp (mk₀ biprod.inl) (α' + β') sorry =
  comp (Y := biprod.{v, u} X X) (mk₀ biprod.inl)
    ((Equiv.symm homEquiv :
        (a : ShiftedHom ((singleFunctor C 0).obj (X ⊞ X)) ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext (X ⊞ X) Y n)
      (HAdd.hAdd (α :=
        ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        α'.hom β'.hom))
    sorry
Tactic: apply biprod_ext