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
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
suffices : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (k : ℕ), d = n + k → e = 0
⊢ HasProjectiveDimensionLT.{v, u} X n

Tactic:
suffices ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext X Y d) (k : ℕ), d = n + k → e = 0 from
    HasProjectiveDimensionLT.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.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + 0
⊢ d = n

Tactic:
simpa using hd
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + 0
⊢ ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y d)

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

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + 0
hX₁ : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y d)
⊢ d = d + 0

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

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y d)
hd : d = d + 0
⊢ e = 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + (k + 1)
succ : ∀ (p : InjectivePresentation.{v, u} Y), e = 0
⊢ e = 0

Tactic:
let ⟨p⟩ := EnoughInjectives.presentation Y
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + (k + 1)
p : InjectivePresentation.{v, u} Y
⊢ ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)

Tactic:
have h : (ShortComplex.mk _ _ (cokernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_cokernel p.f }
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + (k + 1)
p : InjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)
⊢ n + k + 1 = d

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd : d = n + (k + 1)
p : InjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)
⊢ n + k + 1 = d

Tactic:
have hd : n + k + 1 = d := by lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd_1 : d = n + (k + 1)
p : InjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)
hd : n + k + 1 = d
subst :
  ∀ (e : Ext.{w, v, u} X Y (n + k + 1)) (hd : n + k + 1 = n + (k + 1)),
    Eq (α :=
      Ext.{w, v, u} X (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)) (n + k + 1))
      (e.comp (Ext.mk₀ (ShortComplex.f (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯))) ⋯) 0
⊢ Eq (α := Ext.{w, v, u} X (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)) d)
    (e.comp (Ext.mk₀ (ShortComplex.f (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯))) ⋯) 0

Tactic:
subst hd
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
Y : C
p : InjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)
e : Ext.{w, v, u} X Y (n + k + 1)
hd : n + k + 1 = n + (k + 1)
⊢ Eq (α := Ext.{w, v, u} X (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)) (n + k + 1))
    (e.comp (Ext.mk₀ (ShortComplex.f (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯))) ⋯) 0

Tactic:
apply Ext.eq_zero_of_injective

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_injective
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
hd_1 : d = n + (k + 1)
p : InjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)
hd : n + k + 1 = d
succ :
  ∀ (x : Ext.{w, v, u} X (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)) (n + k)),
    x.comp h.extClass hd = 0
⊢ e = 0

Tactic:
obtain ⟨x, rfl⟩ := Ext.covariant_sequence_exact₁ X h e
      (by subst hd; apply Ext.eq_zero_of_injective) hd

Premises used: CategoryTheory.Abelian.Ext.covariant_sequence_exact₁, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
k : ℕ
hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0
d : ℕ
Y : C
hd_1 : d = n + (k + 1)
p : InjectivePresentation.{v, u} Y
h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)
hd : n + k + 1 = d
x : Ext.{w, v, u} X (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) ⋯)) (n + k)
⊢ x.comp h.extClass hd = 0

Tactic:
simp [hk x rfl]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
d : ℕ
Y : C
e : Ext.{w, v, u} X Y d
k : ℕ
hd : d = n + k
zero : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + 0), e = 0
succ :
  ∀ (k : ℕ) (hk : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + k), e = 0) ⦃d : ℕ⦄ ⦃Y : C⦄
    (e : Ext.{w, v, u} X Y 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⟩ := EnoughInjectives.presentation Y
    have h : (ShortComplex.mk _ _ (cokernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_cokernel p.f }
    have hd : n + k + 1 = d := by lia
    obtain ⟨x, rfl⟩ := Ext.covariant_sequence_exact₁ X h e
      (by subst hd; apply Ext.eq_zero_of_injective) hd
    simp [hk x rfl]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 ℕ∞) → (HasProjectiveDimensionLT.{v, u} X a ↔ HasProjectiveDimensionLT.{v, u} Y a)
⊢ Eq (α := WithBot ℕ∞) (sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i})
    (sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} Y i})

Tactic:
congr! 5
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 ℕ∞)
⊢ HasProjectiveDimensionLT.{v, u} X a ↔ HasProjectiveDimensionLT.{v, u} Y a

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

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.hasProjectiveDimensionLT_of_iso
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 ℕ∞)
⊢ HasProjectiveDimensionLT.{v, u} X a ↔ HasProjectiveDimensionLT.{v, u} Y a

Tactic:
exact ⟨fun h ↦ hasProjectiveDimensionLT_of_iso e _,
    fun h ↦ hasProjectiveDimensionLT_of_iso e.symm _⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 ℕ∞) → HasProjectiveDimensionLT.{v, u} Y i} n
simp : ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    (insert ⊤ {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{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.Projective.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 ℕ∞) → HasProjectiveDimensionLT.{v, u} Y i
i : ℕ
hi : n < (↑i : WithBot ℕ∞)
⊢ HasProjectiveDimensionLT.{v, u} Y i

Tactic:
have := hn i hi
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 ℕ∞) → HasProjectiveDimensionLT.{v, u} Y i
i : ℕ
hi : n < (↑i : WithBot ℕ∞)
this : HasProjectiveDimensionLT.{v, u} Y i
⊢ HasProjectiveDimensionLT.{v, u} X i

Tactic:
h.hasProjectiveDimensionLT i

Premises used: CategoryTheory.Retract.hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.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 ℕ∞) → HasProjectiveDimensionLT.{v, u} Y i
i : ℕ
hi : n < (↑i : WithBot ℕ∞)
this : HasProjectiveDimensionLT.{v, u} Y i
⊢ HasProjectiveDimensionLT.{v, u} X i

Tactic:
exact h.hasProjectiveDimensionLT i

Premises used: CategoryTheory.Retract.hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasProjectiveDimensionLT.{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.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
refine_1 : ∀ (h : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)), HasProjectiveDimensionLT.{v, u} X n
refine_2 :
  ∀ (h : HasProjectiveDimensionLT.{v, u} X n),
    ∃ (a : WithBot ℕ∞),
      Membership.mem (γ := Set (WithBot ℕ∞))
          {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i} a ∧
        a < (↑n : WithBot ℕ∞)
⊢ projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasProjectiveDimensionLT.{v, u} X n

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i} ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i}
    (projectiveDimension.{v, u} X)

Tactic:
have : projectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)
this : ∀ (i : ℕ), projectiveDimension.{v, u} X < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i
⊢ HasProjectiveDimensionLT.{v, u} X n

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

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

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

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

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

Tactic:
exact ⟨⊥, fun _ _ ↦ hasProjectiveDimensionLT_of_ge _ 0 _ (by simp), by decide⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasProjectiveDimensionLT.{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.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasProjectiveDimensionLT.{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.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
h : HasProjectiveDimensionLT.{v, u} X (n + 1)
⊢ ∃ (a : WithBot ℕ∞),
    Membership.mem (γ := Set (WithBot ℕ∞))
        {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i} a ∧
      a < (↑(n + 1) : WithBot ℕ∞)

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

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

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

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

Tactic:
projectiveDimension_lt_iff

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

Tactic:
exact projectiveDimension_lt_iff

Premises used: CategoryTheory.projectiveDimension_lt_iff
-- 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 = ⊥ ↔ HasProjectiveDimensionLT.{v, u} X 0
rw₁ : projectiveDimension.{v, u} X = ⊥ ↔ projectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞)
rw₂ : projectiveDimension.{v, u} X = ⊥ ↔ projectiveDimension.{v, u} X < 0
rw₃ : projectiveDimension.{v, u} X < (↑⊥ : WithBot ℕ∞) ↔ projectiveDimension.{v, u} X < 0
rw₄ : projectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞) ↔ projectiveDimension.{v, u} X < 0
rw₅ rw₆ : projectiveDimension.{v, u} X < 0 ↔ projectiveDimension.{v, u} X < 0
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X

Tactic:
rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]

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

Tactic:
generalize hd : projectiveDimension X = d

Premises used: CategoryTheory.projectiveDimension
-- 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 = ⊥
bot : ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{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.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : projectiveDimension.{v, u} X = ⊥
⊢ HasProjectiveDimensionLE.{v, u} X 0

Tactic:
simp [← projectiveDimension_le_iff, hd]

Premises used: 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
hd : projectiveDimension.{v, u} X = ⊥
⊢ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n

Tactic:
exact ⟨0, by simp [← projectiveDimension_le_iff, hd]⟩
-- 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 ℕ∞)
coe :
  ∀
    (this :
      (Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∀ (n : ℕ), ¬HasProjectiveDimensionLE.{v, u} X n) ∨
        Eq (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n),
    False
⊢ Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n

Tactic:
by_contra!
-- 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 ℕ∞)
this :
  (Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∀ (n : ℕ), ¬HasProjectiveDimensionLE.{v, u} X n) ∨
    Eq (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ ∃ (n : ℕ), HasProjectiveDimensionLE.{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.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 ℕ∞)
this : ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
coe : ∀ (n : ℕ) (hn : HasProjectiveDimensionLE.{v, u} X n), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := this
-- 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 : HasProjectiveDimensionLE.{v, u} X n
⊢ Eq (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊤

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

Premises used: CategoryTheory.projectiveDimension_le_iff, top_le_iff, WithBot.coe_top
-- 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:
ENat.coe_ne_top _ ((WithBot.coe_eq_coe).1 hn)

Premises used: Iff.mp, ENat.coe_ne_top, WithBot.coe_eq_coe