awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : projectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
n : ℕ
hn : Eq (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊤
⊢ False

Tactic:
exact ENat.coe_ne_top _ ((WithBot.coe_eq_coe).1 hn)

Premises used: Iff.mp, ENat.coe_ne_top, WithBot.coe_eq_coe
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ
hd : projectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)
coe : ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ Ne (α := WithBot ℕ∞) (↑(↑d : ℕ∞) : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n

Tactic:
simp only [ne_eq, WithBot.coe_eq_top, ENat.coe_ne_top, not_false_eq_true, true_iff]

Premises used: WithBot.coe_eq_top, true_iff, ne_eq, ENat.coe_ne_top, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ
hd : projectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)
⊢ HasProjectiveDimensionLE.{v, u} X d

Tactic:
simpa only [← projectiveDimension_le_iff] using hd.le

Premises used: Eq.le, CategoryTheory.projectiveDimension_le_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ
hd : projectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)
⊢ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n

Tactic:
exact ⟨d, by simpa only [← projectiveDimension_le_iff] using hd.le⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ∞
hd : projectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)
coe :
  ∀ (hd : projectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)),
    Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
coe₁ :
  ∀ (d : ℕ) (hd : projectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)),
    Ne (α := WithBot ℕ∞) (↑(↑d : ℕ∞) : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n

Tactic:
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⟩

Premises used: WithBot.coe_eq_top, false_and, true_iff, not_true_eq_false, false_or, ne_eq, CategoryTheory.projectiveDimension_le_iff, top_le_iff, WithBot.coe_top, ENat.coe_ne_top, not_false_eq_true, true_and
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
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
coe :
  ∀ (d : ℕ∞) (hd : projectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)),
    (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ d ≠ ⊤ ↔ ∃ (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⟩

Premises used: WithBot.coe_eq_top, false_and, true_iff, not_true_eq_false, false_or, ne_eq, CategoryTheory.projectiveDimension_le_iff, top_le_iff, WithBot.coe_top, ENat.coe_ne_top, bot_ne_top, not_false_eq_true, true_and
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
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
rw₆ rw₇ :
  projectiveDimension.{v, u} X ≤ 0 ∧ 0 ≤ projectiveDimension.{v, u} X ↔
    projectiveDimension.{v, u} X ≤ 0 ∧ 0 ≤ projectiveDimension.{v, u} X
⊢ projectiveDimension.{v, u} X = 0 ↔ Projective.{v, u} X ∧ ¬Limits.IsZero.{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]

Premises used: CategoryTheory.projectiveDimension_le_iff, not_lt, le_antisymm_iff, CategoryTheory.projectiveDimension_eq_bot_iff, Nat.cast_zero, WithBot.lt_zero_iff_eq_bot, CategoryTheory.projective_iff_hasProjectiveDimensionLE_zero
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℕ
⊢ R.cochainComplex.IsKProjective

Tactic:
isKProjective_of_projective _ 0

Premises used: CochainComplex.isKProjective_of_projective, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℕ
⊢ QuasiIso R.π'

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℤ)
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 ⋯ (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))) ⋯)
⊢ 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))) ⋯)
      ⋯)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 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 ⋯ (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))) ⋯)

Tactic:
(ShiftedHom.comp_mk₀_id ..).symm

Premises used: CategoryTheory.ShiftedHom.comp_mk₀_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 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 ⋯ (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))) ⋯)

Tactic:
exact (ShiftedHom.comp_mk₀_id ..).symm

Premises used: CategoryTheory.ShiftedHom.comp_mk₀_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℤ)
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)
⊢ (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
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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
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)
⊢ (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:
obtain ⟨x, rfl⟩ := x.mk_surjective

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℤ)
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)
⊢ (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 ⟨y, rfl⟩ := y.mk_surjective

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℤ)
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
⊢ (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:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℤ)
⊢ 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:
simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

Premises used: CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.ShiftedHom.map, CochainComplex.HomComplex.CohomologyClass.mk_add
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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.toFun (Equiv.symm R.extEquivCohomologyClass) (x + y) =
      HAdd.hAdd (α := Ext.{w, v, u} X Y n) (Equiv.toFun (Equiv.symm R.extEquivCohomologyClass) x)
        (Equiv.toFun (Equiv.symm R.extEquivCohomologyClass) y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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) =
    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)
          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:
R.extAddEquivCohomologyClass.symm.map_sub _ _

Premises used: CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, AddEquiv.map_sub, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass, AddEquiv.symm
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : CohomologyClass R.cochainComplex (Functor.obj (singleFunctor C 0) Y) (↑n : ℤ)
⊢ Eq.{w + 1} (α := 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)
          x :
      Ext.{w, v, u} X Y n)

Tactic:
R.extAddEquivCohomologyClass.symm.map_neg _

Premises used: CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, AddEquiv.map_neg, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass, AddEquiv.symm
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
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 : ℕ
⊢ Eq.{w + 1} (α := 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)
      0)
    0

Tactic:
R.extAddEquivCohomologyClass.symm.map_zero

Premises used: AddEquiv.map_zero, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass, AddEquiv.symm