awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
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)
⊢ HasProjectiveDimensionLT.{v, u} X n
have suffices : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (k : ℕ), d = n + k → e = 0
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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
⊢ e = 0
have hX₁ : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y d)
Tactic: obtain rfl : d = n := by simpa using hd
Cleared hypotheses: n, hX, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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)
⊢ e = 0
have hd₁ : d = d + 0
Tactic: obtain rfl : d = n := by simpa using hd
Cleared hypotheses: n, hX, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
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)
⊢ e = 0
have succ : ∀ (p : InjectivePresentation.{v, u} Y), e = 0
Tactic: let ⟨p⟩ := EnoughInjectives.presentation Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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
⊢ e = 0
have h : ShortComplex.ShortExact (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) sorry)
Tactic: have h : (ShortComplex.mk _ _ (cokernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_cokernel p.f }
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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) ⋯)
⊢ e = 0
have hd₁ : n + k + 1 = d
Tactic: have hd : n + k + 1 = d := by lia
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
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
⊢ 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
have 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) sorry)) (n + k + 1))
    (e.comp (Ext.mk₀ (ShortComplex.f (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) sorry))) sorry) 0
Tactic: subst hd
Cleared hypotheses: d, e, hd_1, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
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
⊢ e = 0
have succ : ∀ (x : Ext.{w, v, u} X (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel p.f) p.f (cokernel.π p.f) sorry)) (n + k)),
  x.comp h.extClass hd = 0
Tactic: obtain ⟨x, rfl⟩ := Ext.covariant_sequence_exact₁ X h e
      (by subst hd; apply Ext.eq_zero_of_injective) hd
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
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
⊢ e = 0
have zero : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (hd : d = n + 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]
Cleared hypotheses: d, Y, e, k, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
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
⊢ e = 0
have 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
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]
Cleared hypotheses: d, Y, e, k, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
e : X ≅ Y
⊢ 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})
have h : ∀ (x : WithBot ℕ∞) (a : ℕ),
  x < (↑a : WithBot ℕ∞) → (HasProjectiveDimensionLT.{v, u} X a ↔ HasProjectiveDimensionLT.{v, u} Y a)
Tactic: congr! 5
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X 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
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    (insert ⊤ {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i}) n
have simp : ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i
Tactic: simp only [Set.mem_setOf_eq, not_top_lt, IsEmpty.forall_iff, implies_true,
      Set.insert_eq_of_mem] at hn ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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} X i
have this : HasProjectiveDimensionLT.{v, u} Y i
Tactic: have := hn i hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasProjectiveDimensionLT.{v, u} X n
have refine_1 : ∀ (h : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)), HasProjectiveDimensionLT.{v, u} X n
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
refine_1 : ∀ (h : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)), HasProjectiveDimensionLT.{v, u} X n
⊢ projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasProjectiveDimensionLT.{v, u} X n
have 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 ℕ∞)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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 ℕ∞)
⊢ HasProjectiveDimensionLT.{v, u} X n
have this : 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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
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 ℕ∞)
have 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 ℕ∞)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
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 ℕ∞)
⊢ ∃ (a : WithBot ℕ∞),
    Membership.mem (γ := Set (WithBot ℕ∞))
        {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasProjectiveDimensionLT.{v, u} X i} a ∧
      a < (↑n : WithBot ℕ∞)
have 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 ℕ∞)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ (↑n : WithBot ℕ∞) ≤ projectiveDimension.{v, u} X ↔ ¬HasProjectiveDimensionLT.{v, u} X n
have contrapose! : projectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasProjectiveDimensionLT.{v, u} X n
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw : projectiveDimension.{v, u} X = ⊥ ↔ HasProjectiveDimensionLT.{v, u} X 0
Tactic: rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = ⊥ ↔ HasProjectiveDimensionLT.{v, u} X 0
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₁ : projectiveDimension.{v, u} X = ⊥ ↔ projectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞)
Tactic: rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = ⊥ ↔ HasProjectiveDimensionLT.{v, u} X 0
rw₁ : projectiveDimension.{v, u} X = ⊥ ↔ projectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞)
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₂ : projectiveDimension.{v, u} X = ⊥ ↔ projectiveDimension.{v, u} X < 0
Tactic: rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = ⊥ ↔ 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
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₃ : projectiveDimension.{v, u} X < (↑⊥ : WithBot ℕ∞) ↔ projectiveDimension.{v, u} X < 0
Tactic: rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = ⊥ ↔ 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
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₄ : projectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞) ↔ projectiveDimension.{v, u} X < 0
Tactic: rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
rw : projectiveDimension.{v, u} X = ⊥ ↔ 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
⊢ projectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₅ : projectiveDimension.{v, u} X < 0 ↔ projectiveDimension.{v, u} X < 0
Tactic: rw [← hasProjectiveDimensionLT_zero_iff_isZero, ← projectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ projectiveDimension.{v, u} X ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have generalize : ∀ (d : WithBot ℕ∞) (hd : projectiveDimension.{v, u} X = d), d ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
Tactic: generalize hd : projectiveDimension X = d
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : projectiveDimension.{v, u} X = ⊥
⊢ Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have bot : ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
Tactic: simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : projectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
⊢ Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have coe : ∀
  (this :
    (Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∀ (n : ℕ), ¬HasProjectiveDimensionLE.{v, u} X n) ∨
      Eq (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n),
  False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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
⊢ False
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : projectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
this : ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ False
have coe : ∀ (n : ℕ) (hn : HasProjectiveDimensionLE.{v, u} X n), False
Tactic: obtain ⟨n, hn⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
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
⊢ False
have hn₁ : Eq (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊤
Tactic: rw [← projectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ
hd : projectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)
⊢ Ne (α := WithBot ℕ∞) (↑(↑d : ℕ∞) : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have coe : ∃ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ∞
hd : projectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)
⊢ (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have coe : ∀ (hd : projectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)),
  Ne (α := WithBot ℕ∞) (↑⊤ : 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⟩
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : ℕ∞
hd : projectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)
coe :
  ∀ (hd : projectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)),
    Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
⊢ (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have coe₁ : ∀ (d : ℕ) (hd : projectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)),
  Ne (α := WithBot ℕ∞) (↑(↑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⟩
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
d : WithBot ℕ∞
hd : projectiveDimension.{v, u} X = d
⊢ d ≠ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
have bot : ∀ (hd : projectiveDimension.{v, u} X = ⊥), Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasProjectiveDimensionLE.{v, u} X n
Tactic: induction d with
  | bot =>
    simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
    exact ⟨0, by simp [← projectiveDimension_le_iff, hd]⟩
  | coe d =>
    induction d with
    | top =>
      by_contra!
      simp only [WithBot.coe_top, ne_eq, not_true_eq_false, false_and, true_and, false_or] at this
      obtain ⟨n, hn⟩ := this
      rw [← projectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
      exact ENat.coe_ne_top _ ((WithBot.coe_eq_coe).1 hn)
    | coe d =>
      simp only [ne_eq, WithBot.coe_eq_top, ENat.coe_ne_top, not_false_eq_true, true_iff]
      exact ⟨d, by simpa only [← projectiveDimension_le_iff] using hd.le⟩
Cleared hypotheses: d, hd