awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)
this : ∀ (i : ℕ), injectiveDimension.{v, u} X < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i
⊢ HasInjectiveDimensionLT.{v, u} X n

Tactic:
this _ h
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)
this : ∀ (i : ℕ), injectiveDimension.{v, u} X < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i
⊢ HasInjectiveDimensionLT.{v, u} X n

Tactic:
exact this _ h
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasInjectiveDimensionLT.{v, u} X n
refine_2 :
  ∀ (h : HasInjectiveDimensionLT.{v, u} X 0),
    ∃ (a : WithBot ℕ∞),
      Membership.mem (γ := Set (WithBot ℕ∞))
          {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
        a < (↑0 : WithBot ℕ∞)
refine_2₁ :
  ∀ (n : ℕ) (h : HasInjectiveDimensionLT.{v, u} X (n + 1)),
    ∃ (a : WithBot ℕ∞),
      Membership.mem (γ := Set (WithBot ℕ∞))
          {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
        a < (↑(n + 1) : WithBot ℕ∞)
⊢ ∃ (a : WithBot ℕ∞),
    Membership.mem (γ := Set (WithBot ℕ∞))
        {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
      a < (↑n : WithBot ℕ∞)

Tactic:
obtain _ | n := n
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : HasInjectiveDimensionLT.{v, u} X 0
x : ℕ
h_1 : LT.lt (α := WithBot ℕ∞) ⊥ (↑x : WithBot ℕ∞)
⊢ 0 ≤ x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : HasInjectiveDimensionLT.{v, u} X 0
⊢ LT.lt (α := WithBot ℕ∞) ⊥ (↑0 : WithBot ℕ∞)

Tactic:
decide
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
h : HasInjectiveDimensionLT.{v, u} X 0
⊢ ∃ (a : WithBot ℕ∞),
    Membership.mem (γ := Set (WithBot ℕ∞))
        {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
      a < (↑0 : WithBot ℕ∞)

Tactic:
exact ⟨⊥, fun _ _ ↦ hasInjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasInjectiveDimensionLT.{v, u} X (n + 1)
i : ℕ
hi : LT.lt (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑i : WithBot ℕ∞)
⊢ n + 1 ≤ i

Tactic:
simpa using hi
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasInjectiveDimensionLT.{v, u} X (n + 1)
⊢ LT.lt (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑(n + 1) : WithBot ℕ∞)

Tactic:
simp [ENat.WithBot.lt_add_one_iff]

Premises used: ENat.WithBot.lt_add_one_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasInjectiveDimensionLT.{v, u} X (n + 1)
⊢ ∃ (a : WithBot ℕ∞),
    Membership.mem (γ := Set (WithBot ℕ∞))
        {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
      a < (↑(n + 1) : WithBot ℕ∞)

Tactic:
exact ⟨n, fun i hi ↦ hasInjectiveDimensionLT_of_ge _ (n + 1) _ (by simpa using hi),
        by simp [ENat.WithBot.lt_add_one_iff]⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ injectiveDimension.{v, u} X ≤ (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLE.{v, u} X n

Tactic:
simp [← injectiveDimension_lt_iff, ← ENat.WithBot.lt_add_one_iff]

Premises used: CategoryTheory.injectiveDimension_lt_iff, ENat.WithBot.lt_add_one_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
contrapose! : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLT.{v, u} X n
⊢ (↑n : WithBot ℕ∞) ≤ injectiveDimension.{v, u} X ↔ ¬HasInjectiveDimensionLT.{v, u} X n

Tactic:
contrapose!
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLT.{v, u} X n

Tactic:
injectiveDimension_lt_iff

Premises used: CategoryTheory.injectiveDimension_lt_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLT.{v, u} X n

Tactic:
exact injectiveDimension_lt_iff

Premises used: CategoryTheory.injectiveDimension_lt_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : injectiveDimension.{v, u} X = ⊥ ↔ HasInjectiveDimensionLT.{v, u} X 0
rw₁ : injectiveDimension.{v, u} X = ⊥ ↔ injectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞)
rw₂ : injectiveDimension.{v, u} X = ⊥ ↔ injectiveDimension.{v, u} X < 0
rw₃ : injectiveDimension.{v, u} X < (↑⊥ : WithBot ℕ∞) ↔ injectiveDimension.{v, u} X < 0
rw₄ : injectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞) ↔ injectiveDimension.{v, u} X < 0
rw₅ rw₆ : injectiveDimension.{v, u} X < 0 ↔ injectiveDimension.{v, u} X < 0
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X

Tactic:
rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]

Premises used: CategoryTheory.injectiveDimension_lt_iff, WithBot.lt_coe_bot, Nat.cast_zero, CategoryTheory.hasInjectiveDimensionLT_zero_iff_isZero, bot_eq_zero', WithBot.coe_zero
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
generalize :
  ∀ (d : WithBot ℕ∞) (hd : injectiveDimension.{v, u} X = d), d ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
⊢ injectiveDimension.{v, u} X ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n

Tactic:
generalize hd : injectiveDimension X = d

Premises used: CategoryTheory.injectiveDimension
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = ⊥
bot : ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
⊢ Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n

Tactic:
simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]

Premises used: true_iff, ne_eq, bot_ne_top, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = ⊥
⊢ HasInjectiveDimensionLE.{v, u} X 0

Tactic:
simp [← injectiveDimension_le_iff, hd]

Premises used: CategoryTheory.injectiveDimension_le_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = ⊥
⊢ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n

Tactic:
exact ⟨0, by simp [← injectiveDimension_le_iff, hd]⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
coe :
  ∀
    (this :
      (Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∀ (n : ℕ), ¬HasInjectiveDimensionLE.{v, u} X n) ∨
        Eq (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n),
    False
⊢ Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n

Tactic:
by_contra!
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
this :
  (Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∀ (n : ℕ), ¬HasInjectiveDimensionLE.{v, u} X n) ∨
    Eq (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
⊢ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n

Tactic:
simp only [WithBot.coe_top, ne_eq, not_true_eq_false, false_and, true_and, false_or] at this

Premises used: false_and, not_true_eq_false, false_or, ne_eq, WithBot.coe_top, true_and
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
this : ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
coe : ∀ (n : ℕ) (hn : HasInjectiveDimensionLE.{v, u} X n), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := this
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
n : ℕ
hn : HasInjectiveDimensionLE.{v, u} X n
⊢ Eq (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊤

Tactic:
rw [← injectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn

Premises used: CategoryTheory.injectiveDimension_le_iff, top_le_iff, WithBot.coe_top
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
n : ℕ
hn : Eq (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊤
⊢ False

Tactic:
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.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{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.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ
hd : injectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)
coe : ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
⊢ Ne (α := WithBot ℕ∞) (↑(↑d : ℕ∞) : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{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.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ
hd : injectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)
⊢ HasInjectiveDimensionLE.{v, u} X d

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

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

Tactic:
exact ⟨d, by simpa only [← injectiveDimension_le_iff] using hd.le⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ∞
hd : injectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)
coe :
  ∀ (hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)),
    Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
coe₁ :
  ∀ (d : ℕ) (hd : injectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)),
    Ne (α := WithBot ℕ∞) (↑(↑d : ℕ∞) : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
⊢ (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{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 [← injectiveDimension_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 [← injectiveDimension_le_iff] using hd.le⟩

Premises used: CategoryTheory.injectiveDimension_le_iff, WithBot.coe_eq_top, false_and, true_iff, not_true_eq_false, false_or, ne_eq, top_le_iff, WithBot.coe_top, ENat.coe_ne_top, not_false_eq_true, true_and
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : WithBot ℕ∞
hd : injectiveDimension.{v, u} X = d
bot : ∀ (hd : injectiveDimension.{v, u} X = ⊥), Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
coe :
  ∀ (d : ℕ∞) (hd : injectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)),
    (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
⊢ d ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{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 [← injectiveDimension_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 [← injectiveDimension_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 [← injectiveDimension_le_iff] using hd.le⟩

Premises used: CategoryTheory.injectiveDimension_le_iff, WithBot.coe_eq_top, false_and, true_iff, not_true_eq_false, false_or, ne_eq, top_le_iff, WithBot.coe_top, ENat.coe_ne_top, bot_ne_top, not_false_eq_true, true_and
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
⊢ R.cochainComplex.IsKInjective

Tactic:
isKInjective_of_injective _ 0

Premises used: CochainComplex.isKInjective_of_injective, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
⊢ QuasiIso R.ι'

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
inst_3 : HasDerivedCategory.{u_1, v, u} C
x : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
e_g :
  Eq.{u_1 + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{u_1, v, u} C) (Functor.obj DerivedCategory.Q R.cochainComplex)
      (Functor.obj DerivedCategory.Q (Functor.obj (singleFunctor C 0) Y)))
    (inv (Functor.map DerivedCategory.Q R.ι'))
    (inv (Functor.map DerivedCategory.Q R.ι') ≫ 𝟙 (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.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
              (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
          x)
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 ⋯ (inv (Functor.map DerivedCategory.Q R.ι'))) ⋯)
    (ShiftedHom.comp
      (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) →
              (singleFunctor C 0).obj X ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj R.cochainComplex)
          x)
        DerivedCategory.Q)
      (ShiftedHom.mk₀ 0 ⋯
        (inv (Functor.map DerivedCategory.Q R.ι') ≫ 𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y)))
      ⋯)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
x y : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
have :
  ∀ (this : HasDerivedCategory C),
    (Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            x :
          Ext.{w, v, u} X Y n)
        ((Equiv.symm R.extEquivCohomologyClass :
              (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            y :
          Ext.{w, v, u} X Y n)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          x :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          y :
        Ext.{w, v, u} X Y n)

Tactic:
have := HasDerivedCategory.standard C
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
x y : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
this : HasDerivedCategory C
obtain :
  ∀ (x : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)),
    (Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk x) :
          Ext.{w, v, u} X Y n)
        ((Equiv.symm R.extEquivCohomologyClass :
              (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            y :
          Ext.{w, v, u} X Y n)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          x :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
y : CohomologyClass (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
this : HasDerivedCategory C
x : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)
obtain :
  ∀ (y : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑n : ℤ)),
    (Equiv.symm R.extEquivCohomologyClass :
          (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk x) :
          Ext.{w, v, u} X Y n)
        ((Equiv.symm R.extEquivCohomologyClass :
              (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk y) :
          Ext.{w, v, u} X Y n)
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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.Injective.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 : InjectiveResolution.{v, u} Y
n : ℕ
this : HasDerivedCategory C
x y : Cocycle (Functor.obj (singleFunctor C 0) X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk x) :
          Ext.{w, v, u} X Y n)
        ((Equiv.symm R.extEquivCohomologyClass :
              (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
            (CohomologyClass.mk y) :
          Ext.{w, v, u} X Y n)).hom
⊢ (Equiv.symm R.extEquivCohomologyClass :
        (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑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 ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk x) :
        Ext.{w, v, u} X Y n)
      ((Equiv.symm R.extEquivCohomologyClass :
            (a : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex (↑n : ℤ)) → Ext X Y n)
          (CohomologyClass.mk y) :
        Ext.{w, v, u} X Y n)

Tactic:
ext