From c62eca659a728a18695f430580ac3075b6525dd2 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 12 May 2026 03:47:27 -0600 Subject: [PATCH 1/2] dupe --- Mathlib/SetTheory/Ordinal/Basic.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 64448c9a6278fe..b766f1e9cd8304 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -219,11 +219,15 @@ theorem nonempty_toType_iff {o : Ordinal} : Nonempty o.ToType ↔ o ≠ 0 := by @[deprecated (since := "2026-02-18")] alias toType_nonempty_iff_ne_zero := nonempty_toType_iff +instance instNeZeroOne : NeZero (1 : Ordinal) := + ⟨type_ne_zero_of_nonempty _⟩ + +@[deprecated _root_.one_ne_zero (since := "2026-05-12")] protected theorem one_ne_zero : (1 : Ordinal) ≠ 0 := - type_ne_zero_of_nonempty _ + _root_.one_ne_zero instance nontrivial : Nontrivial Ordinal.{u} := - ⟨⟨1, 0, Ordinal.one_ne_zero⟩⟩ + ⟨⟨1, 0, one_ne_zero⟩⟩ /-- `Quotient.inductionOn` specialized to ordinals. @@ -357,9 +361,6 @@ protected theorem eq_zero_or_pos : ∀ a : Ordinal, a = 0 ∨ 0 < a := eq_bot_or instance : ZeroLEOneClass Ordinal := ⟨bot_le⟩ -instance instNeZeroOne : NeZero (1 : Ordinal) := - ⟨Ordinal.one_ne_zero⟩ - theorem type_le_iff {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s] : type r ≤ type s ↔ Nonempty (r ≼i s) := Iff.rfl From 6b2bcbe13f3a68b6f6c6b61092db17348f570909 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 12 May 2026 03:49:00 -0600 Subject: [PATCH 2/2] fix --- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 2 +- Mathlib/SetTheory/Ordinal/Exponential.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index a25f56cec27bb3..3dc7d66e3f3a3f 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -793,7 +793,7 @@ theorem mul_div_mul_cancel {a : Ordinal} (ha : a ≠ 0) (b c) : a * b / (a * c) @[simp] theorem div_one (a : Ordinal) : a / 1 = a := by - simpa only [one_mul] using mul_div_cancel a Ordinal.one_ne_zero + simpa only [one_mul] using mul_div_cancel a one_ne_zero @[simp] theorem div_self {a : Ordinal} (h : a ≠ 0) : a / a = 1 := by diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index 85e800cddcb778..b048580cc5759b 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -91,7 +91,7 @@ theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by simp only [opow_succ, ih, mul_one] | limit b l IH => refine eq_of_forall_ge_iff fun c => ?_ - rw [opow_le_of_isSuccLimit Ordinal.one_ne_zero l] + rw [opow_le_of_isSuccLimit one_ne_zero l] exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩ theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by @@ -198,7 +198,7 @@ theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b := b rcases le_or_gt a 1 with a1 | a1 · rcases lt_or_eq_of_le a1 with a0 | a1 · rw [lt_one_iff] at a0 - rw [a0, zero_opow Ordinal.one_ne_zero] + rw [a0, zero_opow one_ne_zero] exact zero_le rw [a1, one_opow, one_opow] rwa [opow_le_opow_iff_right a1, one_le_iff_pos]