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
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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
e_a :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.fst)))
      α.hom ⋯)
    α.hom
e_a₁ :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (Functor.map (singleFunctor C 0)
          (CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) biprod.fst)))
      α.hom ⋯)
    α.hom
e_a₂ :
  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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (𝟙 X))) α.hom ⋯) α.hom
e_a₃ :
  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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (𝟙 (Functor.obj (singleFunctor C 0) X))) α.hom ⋯) α.hom
⊢ 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) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.fst)) α.hom ⋯) ⋯)
    α.hom
have e_a₄ : 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: rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_fst, Functor.map_id, ShiftedHom.mk₀_id_comp]
-- 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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
⊢ 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) (biprod.{v, u} X X))
      (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) (hom (comp (mk₀ biprod.snd) β ⋯)) ⋯)
    β.hom
have e_a : 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) (biprod.{v, u} X X))
    (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
    (ShiftedHom.comp (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.snd)) β.hom sorry) sorry)
  β.hom
Tactic: rw [comp_hom, mk₀_hom, mk₀_hom]
-- 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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
⊢ 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) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.snd)) β.hom ⋯) ⋯)
    β.hom
have e_a : 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
    (ShiftedHom.mk₀ 0 mk₀._proof_1
      (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
        (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.snd)))
    β.hom sorry)
  β.hom
Tactic: rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]
-- 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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
e_a :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.snd)))
      β.hom ⋯)
    β.hom
⊢ 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) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.snd)) β.hom ⋯) ⋯)
    β.hom
have e_a₁ : 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
    (ShiftedHom.mk₀ 0 mk₀._proof_1
      (Functor.map (singleFunctor C 0)
        (CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) biprod.snd)))
    β.hom sorry)
  β.hom
Tactic: rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]
-- 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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
e_a :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.snd)))
      β.hom ⋯)
    β.hom
e_a₁ :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (Functor.map (singleFunctor C 0)
          (CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) biprod.snd)))
      β.hom ⋯)
    β.hom
⊢ 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) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.snd)) β.hom ⋯) ⋯)
    β.hom
have e_a₂ : 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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (𝟙 X))) β.hom sorry) β.hom
Tactic: rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]
-- 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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
e_a :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.snd)))
      β.hom ⋯)
    β.hom
e_a₁ :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (Functor.map (singleFunctor C 0)
          (CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) biprod.snd)))
      β.hom ⋯)
    β.hom
e_a₂ :
  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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (𝟙 X))) β.hom ⋯) β.hom
⊢ 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) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.snd)) β.hom ⋯) ⋯)
    β.hom
have e_a₃ : 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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (𝟙 (Functor.obj (singleFunctor C 0) X))) β.hom sorry) β.hom
Tactic: rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]
-- 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))) (α' + β') ⋯
eq₂ :
  α' + β' =
    (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)
e_a :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) (biprod.{v, u} X X))
          (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))) (Functor.map (singleFunctor C 0) biprod.snd)))
      β.hom ⋯)
    β.hom
e_a₁ :
  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
      (ShiftedHom.mk₀ 0 mk₀._proof_1
        (Functor.map (singleFunctor C 0)
          (CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) biprod.snd)))
      β.hom ⋯)
    β.hom
e_a₂ :
  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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (𝟙 X))) β.hom ⋯) β.hom
e_a₃ :
  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 (ShiftedHom.mk₀ 0 mk₀._proof_1 (𝟙 (Functor.obj (singleFunctor C 0) X))) β.hom ⋯) β.hom
⊢ 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) (biprod.{v, u} X X))
      (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) (biprod.lift (𝟙 X) (𝟙 X))))
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 mk₀._proof_1 (Functor.map (singleFunctor C 0) biprod.snd)) β.hom ⋯) ⋯)
    β.hom
have e_a₄ : 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: rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]
-- 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
⊢ 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)
have rw : 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 =
  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)
Tactic: rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]
-- 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
rw :
  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 =
    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)
⊢ 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)
have rw₁ : (α + -α).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)
Tactic: rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]
-- 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
rw :
  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 =
    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)
rw₁ :
  (α + -α).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)
⊢ 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)
have rw₂ : hom.{w', w, v, u} 0 =
  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)
Tactic: rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]
-- 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
rw :
  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 =
    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)
rw₁ :
  (α + -α).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)
rw₂ :
  hom.{w', w, v, u} 0 =
    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)
⊢ 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)
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.{w', w, v, u} 0) 0
Tactic: rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]
-- 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
rw :
  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 =
    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)
rw₁ :
  (α + -α).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)
rw₂ :
  hom.{w', w, v, u} 0 =
    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)
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.{w', w, v, u} 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 (-α.hom)
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 [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]