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 X' : C
e : X ≅ X'
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} X n
⊢ HasInjectiveDimensionLT.{v, u} X' n

Tactic:
e.symm.retract.hasInjectiveDimensionLT n

Premises used: CategoryTheory.Iso.retract, CategoryTheory.Retract.hasInjectiveDimensionLT, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₁ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₃ n
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₂ i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} S.X₂ n

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₁ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₃ n
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
obtain : ∀ (x₃ : Ext Y S.X₁ i), x₃.comp (Ext.mk₀ S.f) ⋯ = 0
⊢ x₂ = 0

Tactic:
obtain ⟨x₃, rfl⟩ := Ext.covariant_sequence_exact₂ _ hS x₂
    (Ext.eq_zero_of_hasInjectiveDimensionLT _ n hi)

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.Abelian.Ext.covariant_sequence_exact₂, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₁ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₃ n
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext Y S.X₁ i
rw : Eq (α := Ext Y S.X₂ i) (Ext.comp 0 (Ext.mk₀ S.f) ⋯) 0
rw₁ rw₂ : Eq (α := Ext Y S.X₂ i) 0 0
⊢ x₃.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
rw [x₃.eq_zero_of_hasInjectiveDimensionLT n hi, Ext.zero_comp]

Premises used: CategoryTheory.Abelian.Ext.zero_comp, CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₃ n
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n + 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₁ i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} S.X₁ (n + 1)

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₃ n
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
hi : n + 1 ≤ 0
Y : C
x₃ : Ext Y S.X₁ 0
⊢ x₃ = 0

Tactic:
simp at hi
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₃ n
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext Y S.X₁ (i + 1)
succ : ∀ (x₁ : Ext Y S.X₃ i), x₁.comp hS.extClass ⋯ = 0
⊢ x₃ = 0

Tactic:
obtain ⟨x₁, rfl⟩ := Ext.covariant_sequence_exact₁ _ hS x₃
      (Ext.eq_zero_of_hasInjectiveDimensionLT _ (n + 1) hi) rfl

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₃ n
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.X₃ i
⊢ n ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT.{v, u} S.X₃ n
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.X₃ i
succ : Eq (α := Ext Y S.X₁ (i + 1)) (Ext.comp 0 hS.extClass ⋯) 0
succ₁ succ₂ : Eq (α := Ext Y S.X₁ (i + 1)) 0 0
⊢ x₁.comp hS.extClass ⋯ = 0

Tactic:
rw [x₁.eq_zero_of_hasInjectiveDimensionLT n (by lia), Ext.zero_comp]

Premises used: CategoryTheory.Abelian.Ext.zero_comp, CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₁ (n + 1)
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0
⊢ HasInjectiveDimensionLT.{v, u} S.X₃ n

Tactic:
rw [hasInjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasInjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₁ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext Y S.X₃ i
⊢ n + 1 ≤ 1 + i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₁ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext Y S.X₃ i
obtain : ∀ (x₂ : Ext Y S.X₂ i), x₂.comp (Ext.mk₀ S.g) ⋯ = 0
⊢ x₁ = 0

Tactic:
obtain ⟨x₂, rfl⟩ := Ext.covariant_sequence_exact₃ _ hS x₁ (add_comm _ _)
    (Ext.eq_zero_of_hasInjectiveDimensionLT _ (n + 1) (by lia))

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃, add_comm, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₁ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
⊢ n ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasInjectiveDimensionLT.{v, u} S.X₁ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext Y S.X₂ i
rw : Eq (α := Ext Y S.X₃ i) (Ext.comp 0 (Ext.mk₀ S.g) ⋯) 0
rw₁ rw₂ : Eq (α := Ext Y S.X₃ i) 0 0
⊢ x₂.comp (Ext.mk₀ S.g) ⋯ = 0

Tactic:
rw [x₂.eq_zero_of_hasInjectiveDimensionLT n (by lia), Ext.zero_comp]

Premises used: CategoryTheory.Abelian.Ext.zero_comp, CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : Injective.{v, u} S.X₂
⊢ HasInjectiveDimensionLT.{v, u} S.X₃ (n + 1) ↔ HasInjectiveDimensionLT.{v, u} S.X₁ (n + 2)

Tactic:
⟨fun _ ↦ hS.hasInjectiveDimensionLT_X₁ (n + 1) inferInstance inferInstance,
    fun _ ↦ hS.hasInjectiveDimensionLT_X₃ (n + 1) inferInstance inferInstance⟩

Premises used: CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁, inferInstance, HAdd.hAdd, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃, Iff.intro, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
n : ℕ
inst_2 : HasInjectiveDimensionLT.{v, u} X n
inst_3 : HasInjectiveDimensionLT.{v, u} Y n
⊢ HasInjectiveDimensionLT.{v, u} (biprod.{v, u} X Y) n

Tactic:
(ShortComplex.Splitting.ofHasBinaryBiproduct X Y).shortExact.hasInjectiveDimensionLT_X₂ n ‹_› ‹_›

Premises used: CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct, CategoryTheory.ShortComplex.Splitting.shortExact, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₂
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (k : ℕ), d = n + k → e = 0
i : ℕ
hi : n ≤ i
Y : C
e : Ext.{w, v, u} Y X i
obtain : ∀ (k : ℕ) (hi : n ≤ n + k) (e : Ext.{w, v, u} Y X (n + k)), e = 0
⊢ e = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext.{w, v, u} Y X (n + k)
⊢ e = 0

Tactic:
this e k rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext.{w, v, u} Y X (n + k)
⊢ e = 0

Tactic:
exact this e k rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
suffices : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (k : ℕ), d = n + k → e = 0
⊢ HasInjectiveDimensionLT.{v, u} X n

Tactic:
suffices ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext Y X d) (k : ℕ), d = n + k → e = 0 from
    HasInjectiveDimensionLT.mk (fun i hi Y e ↦ by
      obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi
      exact this e k rfl)
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + 0
⊢ d = n

Tactic:
simpa using hd
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + 0
⊢ ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X d)

Tactic:
obtain rfl : d = n := by simpa using hd

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + 0
hX₁ : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X d)
⊢ d = d + 0

Tactic:
obtain rfl : d = n := by simpa using hd

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X d)
hd : d = d + 0
⊢ e = 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + (k + 1)
succ : ∀ (p : ProjectivePresentation.{v, u} Y), e = 0
⊢ e = 0

Tactic:
let ⟨p⟩ := EnoughProjectives.presentation Y
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + (k + 1)
p : ProjectivePresentation.{v, u} Y
⊢ ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)

Tactic:
have h : (ShortComplex.mk _ _ (kernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_kernel p.f }
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + (k + 1)
p : ProjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)
⊢ n + k + 1 = d

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd : d = n + (k + 1)
p : ProjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)
⊢ n + k + 1 = d

Tactic:
have hd : (n + k) + 1 = d := by lia
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd_1 : d = n + (k + 1)
p : ProjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)
hd : n + k + 1 = d
subst :
  ∀ (e : Ext.{w, v, u} Y X (n + k + 1)) (hd : n + k + 1 = n + (k + 1)),
    Eq.{w + 1} (α :=
      Ext.{w, v, u} (ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)) X (n + k + 1))
      (Ext.comp (Ext.mk₀ (ShortComplex.g (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯))) e ⋯) 0
⊢ Eq.{w + 1} (α := Ext.{w, v, u} (ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)) X d)
    (Ext.comp (Ext.mk₀ (ShortComplex.g (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯))) e ⋯) 0

Tactic:
subst hd
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
Y : C
p : ProjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)
e : Ext.{w, v, u} Y X (n + k + 1)
hd : n + k + 1 = n + (k + 1)
⊢ Eq.{w + 1} (α :=
    Ext.{w, v, u} (ShortComplex.X₂ (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)) X (n + k + 1))
    (Ext.comp (Ext.mk₀ (ShortComplex.g (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯))) e ⋯) 0

Tactic:
apply Ext.eq_zero_of_projective

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_projective
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
hd_1 : d = n + (k + 1)
p : ProjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)
hd : n + k + 1 = d
succ :
  ∀ (x : Ext.{w, v, u} (ShortComplex.X₁ (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)) X (n + k)),
    Ext.comp h.extClass x ⋯ = 0
⊢ e = 0

Tactic:
obtain ⟨x, rfl⟩ := Ext.contravariant_sequence_exact₃ h X e
      (by subst hd; apply Ext.eq_zero_of_projective) ((add_comm _ _).trans hd)

Premises used: add_comm, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃, rfl, Eq.trans
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0
d : ℕ
Y : C
hd_1 : d = n + (k + 1)
p : ProjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)
hd : n + k + 1 = d
x : Ext.{w, v, u} (ShortComplex.X₁ (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f ⋯)) X (n + k)
⊢ Ext.comp h.extClass x ⋯ = 0

Tactic:
simp [hk x rfl]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughProjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} Y X n)
d : ℕ
Y : C
e : Ext.{w, v, u} Y X d
k : ℕ
hd : d = n + k
zero : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + 0), e = 0
succ :
  ∀ (k : ℕ) (hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X d) (hd : d = n + k), e = 0) ⦃d : ℕ⦄ ⦃Y : C⦄
    (e : Ext.{w, v, u} Y X d) (hd : d = n + (k + 1)), e = 0
⊢ e = 0

Tactic:
induction k generalizing d Y with
  | zero =>
    obtain rfl : d = n := by simpa using hd
    subsingleton
  | succ k hk =>
    let ⟨p⟩ := EnoughProjectives.presentation Y
    have h : (ShortComplex.mk _ _ (kernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_kernel p.f }
    have hd : (n + k) + 1 = d := by lia
    obtain ⟨x, rfl⟩ := Ext.contravariant_sequence_exact₃ h X e
      (by subst hd; apply Ext.eq_zero_of_projective) ((add_comm _ _).trans hd)
    simp [hk x rfl]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
e : X ≅ Y
h :
  ∀ (x : WithBot ℕ∞) (a : ℕ),
    x < (↑a : WithBot ℕ∞) → (HasInjectiveDimensionLT.{v, u} X a ↔ HasInjectiveDimensionLT.{v, u} Y a)
⊢ Eq (α := WithBot ℕ∞) (sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i})
    (sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i})

Tactic:
congr! 5
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
e : X ≅ Y
x : WithBot ℕ∞
a : ℕ
h : x < (↑a : WithBot ℕ∞)
⊢ HasInjectiveDimensionLT.{v, u} X a ↔ HasInjectiveDimensionLT.{v, u} Y a

Tactic:
⟨fun h ↦ hasInjectiveDimensionLT_of_iso e _,
    fun h ↦ hasInjectiveDimensionLT_of_iso e.symm _⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.hasInjectiveDimensionLT_of_iso
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
e : X ≅ Y
x : WithBot ℕ∞
a : ℕ
h : x < (↑a : WithBot ℕ∞)
⊢ HasInjectiveDimensionLT.{v, u} X a ↔ HasInjectiveDimensionLT.{v, u} Y a

Tactic:
exact ⟨fun h ↦ hasInjectiveDimensionLT_of_iso e _,
    fun h ↦ hasInjectiveDimensionLT_of_iso e.symm _⟩
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn :
  Membership.mem (γ := Set (WithBot ℕ∞))
    {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i} n
simp : ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    (insert ⊤ {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i}) n

Tactic:
simp only [Set.mem_setOf_eq, not_top_lt, IsEmpty.forall_iff, implies_true,
      Set.insert_eq_of_mem] at hn ⊢

Premises used: not_top_lt, Set.insert_eq_of_mem, Set.mem_setOf_eq, implies_true, IsEmpty.forall_iff
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i
i : ℕ
hi : n < (↑i : WithBot ℕ∞)
⊢ HasInjectiveDimensionLT.{v, u} Y i

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

Tactic:
h.hasInjectiveDimensionLT i

Premises used: CategoryTheory.Retract.hasInjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i
i : ℕ
hi : n < (↑i : WithBot ℕ∞)
this : HasInjectiveDimensionLT.{v, u} Y i
⊢ HasInjectiveDimensionLT.{v, u} X i

Tactic:
exact h.hasInjectiveDimensionLT i

Premises used: CategoryTheory.Retract.hasInjectiveDimensionLT
-- 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:
⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩

Premises used: Iff.mpr, sInf_lt_iff, Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
refine_1 : ∀ (h : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)), HasInjectiveDimensionLT.{v, u} X n
refine_2 :
  ∀ (h : HasInjectiveDimensionLT.{v, u} X n),
    ∃ (a : WithBot ℕ∞),
      Membership.mem (γ := Set (WithBot ℕ∞))
          {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
        a < (↑n : WithBot ℕ∞)
⊢ injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLT.{v, u} X n

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
-- 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 ℕ∞)
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} ⊤

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
n : ℕ
h : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i}
    (injectiveDimension.{v, u} X)

Tactic:
have : injectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩