awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : 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)
⊢ e = 0
have succ : ∀ (p : ProjectivePresentation.{v, u} Y), e = 0
Tactic: let ⟨p⟩ := EnoughProjectives.presentation Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : 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
⊢ e = 0
have h : ShortComplex.ShortExact (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f sorry)
Tactic: have h : (ShortComplex.mk _ _ (kernel.condition p.f)).ShortExact :=
      { exact := ShortComplex.exact_kernel p.f }
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : 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 ⋯)
⊢ 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.Injective.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 : 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
⊢ 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
have 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 sorry)) X (n + k + 1))
    (Ext.comp (Ext.mk₀ (ShortComplex.g (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f sorry))) e sorry) 0
Tactic: subst hd
Cleared hypotheses: d, e, hd_1, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : 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
⊢ e = 0
have succ : ∀ (x : Ext.{w, v, u} (ShortComplex.X₁ (ShortComplex.mk (X₁ := kernel p.f) (kernel.ι p.f) p.f sorry)) X (n + k)),
  Ext.comp h.extClass x sorry = 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)
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : 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
⊢ e = 0
have zero : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} Y X 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⟩ := 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]
Cleared hypotheses: d, Y, e, k, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 : 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
⊢ e = 0
have 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
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]
Cleared hypotheses: d, Y, e, k, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 ℕ∞) → HasInjectiveDimensionLT.{v, u} X i})
    (sInf {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i})
have h : ∀ (x : WithBot ℕ∞) (a : ℕ),
  x < (↑a : WithBot ℕ∞) → (HasInjectiveDimensionLT.{v, u} X a ↔ HasInjectiveDimensionLT.{v, u} Y a)
Tactic: congr! 5
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.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 ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i} n
⊢ Membership.mem (γ := Set (WithBot ℕ∞))
    (insert ⊤ {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i}) n
have simp : ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{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.Injective.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 ℕ∞) → HasInjectiveDimensionLT.{v, u} Y i
i : ℕ
hi : n < (↑i : WithBot ℕ∞)
⊢ HasInjectiveDimensionLT.{v, u} X i
have this : HasInjectiveDimensionLT.{v, u} Y i
Tactic: have := hn i hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
have refine_1 : ∀ (h : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞)), HasInjectiveDimensionLT.{v, u} X n
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLT.{v, u} X n
have 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 ℕ∞)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ sInf_lt_iff.2 ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (hypothesis)
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 ℕ∞)
⊢ HasInjectiveDimensionLT.{v, u} X n
have this : 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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
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 ℕ∞)
have 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 ℕ∞)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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 ℕ∞)
⊢ ∃ (a : WithBot ℕ∞),
    Membership.mem (γ := Set (WithBot ℕ∞))
        {n : WithBot ℕ∞ | ∀ (i : ℕ), n < (↑i : WithBot ℕ∞) → HasInjectiveDimensionLT.{v, u} X i} a ∧
      a < (↑n : WithBot ℕ∞)
have 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 ℕ∞)
Tactic: obtain _ | n := n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
⊢ (↑n : WithBot ℕ∞) ≤ injectiveDimension.{v, u} X ↔ ¬HasInjectiveDimensionLT.{v, u} X n
have contrapose! : injectiveDimension.{v, u} X < (↑n : WithBot ℕ∞) ↔ HasInjectiveDimensionLT.{v, u} X n
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw : injectiveDimension.{v, u} X = ⊥ ↔ HasInjectiveDimensionLT.{v, u} X 0
Tactic: rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₁ : injectiveDimension.{v, u} X = ⊥ ↔ injectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞)
Tactic: rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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 ℕ∞)
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₂ : injectiveDimension.{v, u} X = ⊥ ↔ injectiveDimension.{v, u} X < 0
Tactic: rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₃ : injectiveDimension.{v, u} X < (↑⊥ : WithBot ℕ∞) ↔ injectiveDimension.{v, u} X < 0
Tactic: rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₄ : injectiveDimension.{v, u} X < (↑0 : WithBot ℕ∞) ↔ injectiveDimension.{v, u} X < 0
Tactic: rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ injectiveDimension.{v, u} X = ⊥ ↔ Limits.IsZero.{v, u} X
have rw₅ : injectiveDimension.{v, u} X < 0 ↔ injectiveDimension.{v, u} X < 0
Tactic: rw [← hasInjectiveDimensionLT_zero_iff_isZero, ← injectiveDimension_lt_iff,
    Nat.cast_zero, ← WithBot.lt_coe_bot, bot_eq_zero', WithBot.coe_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ injectiveDimension.{v, u} X ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have generalize : ∀ (d : WithBot ℕ∞) (hd : injectiveDimension.{v, u} X = d), d ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
Tactic: generalize hd : injectiveDimension X = d
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = ⊥
⊢ Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have bot : ∃ (n : ℕ), HasInjectiveDimensionLE.{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.Injective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)
⊢ Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have coe : ∀
  (this :
    (Ne (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∀ (n : ℕ), ¬HasInjectiveDimensionLE.{v, u} X n) ∨
      Eq (α := WithBot ℕ∞) (↑⊤ : WithBot ℕ∞) ⊤ ∧ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n),
  False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (hypothesis)
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
⊢ False
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ False
have coe : ∀ (n : ℕ) (hn : HasInjectiveDimensionLE.{v, u} X n), False
Tactic: obtain ⟨n, hn⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (hypothesis)
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
⊢ False
have hn₁ : Eq (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) ⊤
Tactic: rw [← injectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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 ℕ∞)
⊢ Ne (α := WithBot ℕ∞) (↑(↑d : ℕ∞) : WithBot ℕ∞) ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have coe : ∃ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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 ℕ∞)
⊢ (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have coe : ∀ (hd : injectiveDimension.{v, u} X = (↑⊤ : WithBot ℕ∞)),
  Ne (α := WithBot ℕ∞) (↑⊤ : 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⟩
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have coe₁ : ∀ (d : ℕ) (hd : injectiveDimension.{v, u} X = (↑(↑d : ℕ∞) : WithBot ℕ∞)),
  Ne (α := WithBot ℕ∞) (↑(↑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⟩
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ d ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have bot : ∀ (hd : injectiveDimension.{v, u} X = ⊥), Ne (α := WithBot ℕ∞) ⊥ ⊤ ↔ ∃ (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⟩
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Dimension (goal)
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
⊢ d ≠ ⊤ ↔ ∃ (n : ℕ), HasInjectiveDimensionLE.{v, u} X n
have coe : ∀ (d : ℕ∞) (hd : injectiveDimension.{v, u} X = (↑d : WithBot ℕ∞)),
  (↑d : WithBot ℕ∞) ≠ ⊤ ↔ ∃ (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⟩
Cleared hypotheses: d, hd