awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : WithBot ℕ∞
hd : projectiveDimension.{v, u} X = d
bot :
  ∀ (hd : projectiveDimension.{v, u} X = ⊥), Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ d ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have coe : ∀ (d : ℕ∞) (hd : projectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)),
  (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
Tactic: induction d with
  | bot =>
    simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
    exact ⟨0, by simp [← projectiveDimension_le_iff, hd]⟩
  | coe d =>
    induction d with
    | top =>
      by_contra!
      simp only [WithBot.coe_top, ne_eq, not_true_eq_false, false_and, true_and, false_or] at this
      obtain ⟨n, hn⟩ := this
      rw [← projectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
      exact ENat.coe_ne_top _ ((WithBot.coe_eq_coe).1 hn)
    | coe d =>
      simp only [ne_eq, WithBot.coe_eq_top, ENat.coe_ne_top, not_false_eq_true, true_iff]
      exact ⟨d, by simpa only [← projectiveDimension_le_iff] using hd.le⟩
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw₁ : projectiveDimension.{v, u} X = 0 ↔ HasProjectiveDimensionLE.{v, u} X 0 ∧ ¬projectiveDimension.{v, u} X = ⊥
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₁ : projectiveDimension.{v, u} X = 0 ↔ HasProjectiveDimensionLE.{v, u} X 0 ∧ ¬projectiveDimension.{v, u} X = ⊥
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw₂ : projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X = ⊥
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₁ : projectiveDimension.{v, u} X = 0 ↔ HasProjectiveDimensionLE.{v, u} X 0 ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₂ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X = ⊥
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw₃ : projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X < 0
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₁ : projectiveDimension.{v, u} X = 0 ↔ HasProjectiveDimensionLE.{v, u} X 0 ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₂ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₃ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X < 0
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw₄ : projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ 0 ≤ projectiveDimension.{v, u} X
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₁ : projectiveDimension.{v, u} X = 0 ↔ HasProjectiveDimensionLE.{v, u} X 0 ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₂ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₃ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X < 0
rw₄ :
  projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ 0 ≤ projectiveDimension.{v, u} X
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw₅ : projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ 0 ∧ 0 ≤ projectiveDimension.{v, u} X
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₁ : projectiveDimension.{v, u} X = 0 ↔ HasProjectiveDimensionLE.{v, u} X 0 ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₂ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X = ⊥
rw₃ :
  projectiveDimension.{v, u} X = 0 ↔
    projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ ¬projectiveDimension.{v, u} X < 0
rw₄ :
  projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ (↑0 : WithBot ℕ∞) ∧ 0 ≤ projectiveDimension.{v, u} X
rw₅ : projectiveDimension.{v, u} X = 0 ↔ projectiveDimension.{v, u} X ≤ 0 ∧ 0 ≤ projectiveDimension.{v, u} X
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{v, u} X
have rw₆ : projectiveDimension.{v, u} X ≤ 0 ∧ 0 ≤ projectiveDimension.{v, u} X ↔
  projectiveDimension.{v, u} X ≤ 0 ∧ 0 ≤ projectiveDimension.{v, u} X
Tactic: rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
x : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ)
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) X))
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)) (↑n : ℤ))
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
              R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
          x)
        DerivedCategory.Q)
      ⋯)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            x)
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯ (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))) ⋯)
      ⋯)
have e_g : Eq.{u_1 + 1} (α :=
  ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (M := ℤ) (Functor.obj DerivedCategory.Q R.cochainComplex)
    (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)) (↑n : ℤ))
  (ShiftedHom.map
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
          R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
      x)
    DerivedCategory.Q)
  (ShiftedHom.comp
    (ShiftedHom.map
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
            R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
        x)
      DerivedCategory.Q)
    (ShiftedHom.mk₀ 0 sorry (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))) sorry)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
x y : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (x + y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          x :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)
have have : ∀ (this : HasDerivedCategory C),
  (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (x + y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          x :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)
Tactic: have := HasDerivedCategory.standard C
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
x y : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
this : HasDerivedCategory C
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (x + y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          x :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)
have obtain : ∀ (x : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)),
  (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk x + y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
y : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
this : HasDerivedCategory C
x : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk x + y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)
have obtain : ∀ (y : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)),
  (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk x + CohomologyClass.mk y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk y) :
        Ext.{w, v, u} X Y n)
Tactic: obtain ⟨y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
this : HasDerivedCategory C
x y : Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk x + CohomologyClass.mk y) =
    HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk y) :
        Ext.{w, v, u} X Y n)
have h : Eq (α :=
  ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
    (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
  (Ext.hom
    ((Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk x + CohomologyClass.mk y)))
  (HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk y) :
        Ext.{w, v, u} X Y n)).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ HAdd.hAdd (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) (R.extMk g m hm hg) = R.extMk (f + g) m hm ⋯
have simp : HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n) =
  (Equiv.symm R.extEquivCohomologyClass :
      (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
    (CohomologyClass.mk
      (Cocycle.toSingleMk
        ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f + (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ))
        sorry sorry))
Tactic: simp only [extMk, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯ (-(↑m : ℤ)) ⋯ ⋯)) :
        Ext.{w, v, u} X Y n) =
    (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
      (CohomologyClass.mk
        (Cocycle.toSingleMk
          ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f + (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ g) ⋯
          (-(↑m : ℤ)) ⋯ ⋯))
have rw : HAdd.hAdd (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n) =
  (Equiv.symm R.extEquivCohomologyClass :
      (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
    (CohomologyClass.mk
      (HAdd.hAdd (α := Cocycle R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ))
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)
        (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ)) sorry sorry)))
Tactic: rw [Cocycle.toSingleMk_add _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Ext (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
R : ProjectiveResolution.{v, u} X
n : ℕ
f g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ HSub.hSub (α := Ext.{w, v, u} X Y n) (R.extMk f m hm hf) (R.extMk g m hm hg) = R.extMk (f - g) m hm ⋯
have simp : HSub.hSub (α := Ext.{w, v, u} X Y n) (β := Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n)
    ((Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
        (CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ)) sorry sorry)) :
      Ext.{w, v, u} X Y n) =
  (Equiv.symm R.extEquivCohomologyClass :
      (a : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) → Ext X Y n)
    (CohomologyClass.mk
      (Cocycle.toSingleMk
        ((R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ f - (R.cochainComplexXIso (-(↑n : ℤ)) n sorry).hom ≫ g) sorry (-(↑m : ℤ))
        sorry sorry))
Tactic: simp only [extMk, Preadditive.comp_sub]