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

Tactic:
have eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') (zero_add n) := by
    simp [α', β']
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} 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))
      ⋯
h₂ :
  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))
      ⋯
⊢ α' + β' =
    (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:
apply biprod_ext

Premises used: CategoryTheory.Abelian.Ext.biprod_ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
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₁ :
  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) (α' + β') ⋯).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))
        ⋯))
⊢ 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))
      ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
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.{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) (α' + β') ⋯).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))
        ⋯))

Tactic:
simp [α', β', ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_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
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₂ :
  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) (α' + β') ⋯).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))
        ⋯))
⊢ 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))
      ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
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.{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) (α' + β') ⋯).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))
        ⋯))

Tactic:
simp [α', β', ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_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
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)

Tactic:
have eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom) := by
    apply biprod_ext
    all_goals ext; simp [α', β', ← Functor.map_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
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)
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 ⋯)
      (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
⊢ (α + β).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:
simp only [eq₁, eq₂, comp_hom, Equiv.apply_symm_apply, ShiftedHom.comp_add]

Premises used: Equiv.apply_symm_apply, CategoryTheory.ShiftedHom.comp_add, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
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
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

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
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 (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
⊢ 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

Tactic:
dsimp [α']
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
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 (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
⊢ 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

Tactic:
rw [comp_hom, mk₀_hom, mk₀_hom]

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
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 (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
⊢ 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

Tactic:
dsimp [β']
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α β : Ext.{w, v, u} X Y n
α' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.fst) α ⋯
β' : Ext.{w, v, u} (biprod.{v, u} X X) Y n := comp (mk₀ biprod.snd) β ⋯
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 (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
⊢ 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

Tactic:
rw [comp_hom, mk₀_hom, mk₀_hom]

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α : Ext.{w, v, u} X Y n
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
rw₄ rw₅ :
  Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    0 0
⊢ Eq.{w' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (-α).hom (-α.hom)

Tactic:
rw [← add_right_inj α.hom, ← add_hom, add_neg_cancel, add_neg_cancel, zero_hom]

Premises used: add_neg_cancel, CategoryTheory.Abelian.Ext.add_hom, CategoryTheory.Abelian.Ext.zero_hom, CategoryTheory.Abelian.Ext.hom, add_right_inj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y Z T : C
n_1 : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
n : ℕ
⊢ ∀ (x y : Ext.{w, v, u} X Y n),
    Equiv.toFun homEquiv (x + y) =
      HAdd.hAdd (α :=
        ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
          (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        (Equiv.toFun homEquiv x) (Equiv.toFun homEquiv y)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
n : ℕ
inst_3 : HasDerivedCategory.{w', v, u} C
α : Ext.{w, v, u} 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 : ℤ))
    ((homAddEquiv : (a : Ext X Y n) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (↑n : ℤ)) α :
      ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
    (α.hom :
      ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y Z T : C
n a b c : ℕ
h : a + b = c
α : Ext.{w, v, u} X Y a
⊢ ∀ (a_1 b_1 : Ext.{w, v, u} Y Z b),
    (fun (β : Ext.{w, v, u} Y Z b) ↦ α.comp β h) (a_1 + b_1) =
      HAdd.hAdd (α := Ext.{w, v, u} X Z c) ((fun (β : Ext.{w, v, u} Y Z b) ↦ α.comp β h) a_1)
        ((fun (β : Ext.{w, v, u} Y Z b) ↦ α.comp β h) b_1)

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
n a b c : ℕ
h : a + b = c
⊢ ∀ (a_1 b_1 : Ext.{w, v, u} X Y a),
    (fun (α : Ext.{w, v, u} X Y a) ↦
          (AddMonoidHom.mk' (fun (β : Ext.{w, v, u} Y Z b) ↦ α.comp β h) ⋯ :
            Ext.{w, v, u} Y Z b →+ Ext.{w, v, u} X Z c))
        (a_1 + b_1) =
      HAdd.hAdd (α := Ext.{w, v, u} Y Z b →+ Ext.{w, v, u} X Z c)
        ((fun (α : Ext.{w, v, u} X Y a) ↦
            (AddMonoidHom.mk' (fun (β : Ext.{w, v, u} Y Z b) ↦ α.comp β h) ⋯ :
              Ext.{w, v, u} Y Z b →+ Ext.{w, v, u} X Z c))
          a_1)
        ((fun (α : Ext.{w, v, u} X Y a) ↦
            (AddMonoidHom.mk' (fun (β : Ext.{w, v, u} Y Z b) ↦ α.comp β h) ⋯ :
              Ext.{w, v, u} Y Z b →+ Ext.{w, v, u} X Z c))
          b_1)

Tactic:
aesop