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))) (α' + β') ⋯
h₁ :
  comp (mk₀ biprod.inl) (α' + β') ⋯ =
    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))
      ⋯
⊢ α' + β' =
    (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.inr) (α' + β') sorry =
  comp (Y := biprod.{v, u} X X) (mk₀ biprod.inr)
    ((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
-- 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))) (α' + β') ⋯
⊢ comp (mk₀ biprod.inl) (α' + β') ⋯ =
    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))
      ⋯
have 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 : ℤ))
  (comp (mk₀ biprod.inl) (α' + β') sorry).hom
  (hom.{w', w, v, u}
    (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: 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 : ℕ
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))) (α' + β') ⋯
⊢ comp (mk₀ biprod.inr) (α' + β') ⋯ =
    comp (Y := biprod.{v, u} X X) (mk₀ biprod.inr)
      ((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₂ : Eq.{w' + 1} (α :=
  ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
    (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
  (comp (mk₀ biprod.inr) (α' + β') sorry).hom
  (hom.{w', w, v, u}
    (comp (Y := biprod.{v, u} X X) (mk₀ biprod.inr)
      ((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: ext
-- 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) β ⋯
eq₁ : α + β = comp (mk₀ (biprod.lift (𝟙 X) (𝟙 X))) (α' + β') ⋯
⊢ (α + β).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₂ : α' + β' =
  (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)
Tactic: have eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom) := by
    apply biprod_ext
    all_goals ext; simp [α', β', ← Functor.map_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)
⊢ (α + β).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 simp : HAdd.hAdd (α :=
    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} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) α'.hom sorry)
    (ShiftedHom.comp (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) β'.hom sorry) =
  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: simp only [eq₁, eq₂, comp_hom, Equiv.apply_symm_apply, ShiftedHom.comp_add]
-- 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)
⊢ HAdd.hAdd (α :=
      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} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) α'.hom ⋯)
      (ShiftedHom.comp (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) β'.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 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 (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) α'.hom sorry) α.hom
Tactic: congr
-- 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 (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) α'.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 : ℤ))
      (ShiftedHom.comp (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) α'.hom ⋯)
      (ShiftedHom.comp (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) β'.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 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 (hom.{w', w, v, u} (mk₀ (biprod.lift (𝟙 X) (𝟙 X)))) β'.hom sorry) β.hom
Tactic: congr
-- 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.fst) α ⋯)) ⋯)
    α.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.fst)) α.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.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 : ℤ))
  (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 sorry)
  α.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)
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
⊢ 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 : ℤ))
  (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 sorry)
  α.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)
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
⊢ 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 : ℤ))
  (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_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)
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
⊢ 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 : ℤ))
  (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_fst, Functor.map_id, ShiftedHom.mk₀_id_comp]