From 44d323ed88fb45a4fa389e2699cb4baf97eb5283 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Thu, 21 May 2026 00:23:25 -0600 Subject: [PATCH] deprecate --- Mathlib/SetTheory/Cardinal/Aleph.lean | 4 +--- Mathlib/SetTheory/Ordinal/Basic.lean | 3 ++- Mathlib/SetTheory/Ordinal/Exponential.lean | 4 ++-- Mathlib/SetTheory/Ordinal/Notation.lean | 13 +++++++------ 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean index d6c391e9775334..5d077051de1e5a 100644 --- a/Mathlib/SetTheory/Cardinal/Aleph.lean +++ b/Mathlib/SetTheory/Cardinal/Aleph.lean @@ -600,9 +600,7 @@ theorem isNormal_preBeth : Order.IsNormal preBeth := by theorem preBeth_nat : ∀ n : ℕ, preBeth n = (2 ^ ·)^[n] (0 : ℕ) | 0 => by simp - | n + 1 => by - rw [natCast_succ, preBeth_succ, Function.iterate_succ_apply', preBeth_nat] - simp + | n + 1 => by simp [Function.iterate_succ_apply', preBeth_nat] @[simp] theorem preBeth_one : preBeth 1 = 1 := by diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index e21f2a6560ab15..3ae32b127dfa6e 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -953,8 +953,9 @@ protected theorem le_one_iff {a : Ordinal} : a ≤ 1 ↔ a = 0 ∨ a = 1 := theorem card_succ (o : Ordinal) : card (succ o) = card o + 1 := by simp +@[deprecated Nat.cast_add_one (since := "2026-05-21")] theorem natCast_succ (n : ℕ) : ↑n.succ = succ (n : Ordinal) := - rfl + n.cast_add_one instance uniqueIioOne : Unique (Iio (1 : Ordinal)) where default := ⟨0, zero_lt_one' Ordinal⟩ diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index b048580cc5759b..03af43a824c1f6 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -490,8 +490,8 @@ theorem lt_omega0_opow {a b : Ordinal} (hb : b ≠ 0) : refine ⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩, fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩ obtain ⟨n, hn⟩ := lt_omega0.1 (div_opow_log_lt a one_lt_omega0) - use n.succ - rw [natCast_succ, ← hn] + use n + 1 + rw [Nat.cast_add_one, ← hn] exact lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero) theorem lt_omega0_opow_succ {a b : Ordinal} : a < ω ^ succ b ↔ ∃ n : ℕ, a < ω ^ b * n := by diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index 24e16abbcce6fe..3933770caba84b 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -557,7 +557,7 @@ theorem repr_mul : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ * o₂) = rep · obtain ⟨x, xe⟩ := Nat.exists_eq_succ_of_ne_zero n₂.ne_zero simp only [Mul.mul, mul, e0, ↓reduceIte, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul] simp only [xe, h₂.zero_of_zero e0, repr, add_zero] - rw [natCast_succ x, add_mul_succ _ ao, mul_assoc] + rw [Nat.cast_add_one x, ← succ_eq_add_one, add_mul_succ _ ao, mul_assoc] · simp only [repr] haveI := h₁.fst haveI := h₂.fst @@ -842,9 +842,10 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω calc (ω0 ^ (k.succ : Ordinal)) * α' + R' _ = (ω0 ^ succ (k : Ordinal)) * α' + ((ω0 ^ (k : Ordinal)) * α' * m + R) := by - rw [natCast_succ, RR, ← mul_assoc] + rw [Nat.cast_add_one, RR, ← mul_assoc, succ_eq_add_one] _ = ((ω0 ^ (k : Ordinal)) * α' + R) * α' + ((ω0 ^ (k : Ordinal)) * α' + R) * m := ?_ - _ = (α' + m) ^ succ (k.succ : Ordinal) := by rw [← mul_add, natCast_succ, opow_succ, IH.2] + _ = (α' + m) ^ succ (k.succ : Ordinal) := by + rw [← mul_add, opow_succ, Nat.cast_add_one, IH.2, succ_eq_add_one] congr 1 · have αd : ω ∣ α' := dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d @@ -865,7 +866,7 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω · cases m · have : R = 0 := by cases k <;> simp [R, opowAux] simp [this] - · rw [natCast_succ, add_mul_succ] + · rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ] apply add_of_omega0_opow_le Rl rw [opow_mul, opow_succ] gcongr @@ -1010,14 +1011,14 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta refine ⟨isSuccLimit_mul_right this isSuccLimit_omega0, fun i => ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega0'⟩ - rw [← mul_succ, ← natCast_succ] + rw [← mul_add_one, ← Nat.cast_add_one] gcongr apply natCast_lt_omega0 · have := opow_pos (repr a') omega0_pos refine ⟨isSuccLimit_add _ (isSuccLimit_mul_right this isSuccLimit_omega0), fun i => ⟨this, ?_, ?_⟩, exists_lt_add exists_lt_mul_omega0'⟩ - · rw [← mul_succ, ← natCast_succ] + · rw [← mul_add_one, ← Nat.cast_add_one] gcongr apply natCast_lt_omega0 · refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))