fix

Author: vihdzp

Mathlib/SetTheory/Ordinal/FixedPoint.lean

@@ -340,6 +340,7 @@ def deriv (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
 theorem deriv_eq_derivFamily (f : Ordinal → Ordinal) : deriv f = derivFamily fun _ : Unit => f :=
   rfl
 
+-- TODO: rename to `deriv_zero` once the name is available
 @[simp]
 theorem deriv_zero_right (f) : deriv f 0 = nfp f 0 :=
   derivFamily_zero _
@@ -361,6 +362,7 @@ theorem isNormal_deriv (f) : IsNormal (deriv f) :=
 theorem deriv_strictMono (f) : StrictMono (deriv f) :=
   derivFamily_strictMono _
 
+@[deprecated "do not depend on the junk values of `nfp`" (since := "2026-05-13")]
 theorem deriv_eq_id_of_nfp_eq_id (h : nfp f = id) : deriv f = id :=
   ((isNormal_deriv _).ext_iff .id).2 (by simp [h])
 
@@ -396,6 +398,7 @@ theorem deriv_eq_enumOrd (H : IsNormal f) : deriv f = enumOrd (Function.fixedPoi
   convert derivFamily_eq_enumOrd fun _ : Unit => H
   exact (Set.iInter_const _).symm
 
+@[deprecated "do not depend on the junk values of `nfp`" (since := "2026-05-13")]
 theorem nfp_zero_left (a) : nfp 0 a = a := by
   rw [← iSup_iterate_eq_nfp]
   apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)
@@ -405,15 +408,19 @@ theorem nfp_zero_left (a) : nfp 0 a = a := by
   · rw [Function.iterate_succ']
     simp
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "do not depend on the junk values of `nfp`" (since := "2026-05-13")]
 theorem nfp_zero : nfp 0 = id := by
   ext
   exact nfp_zero_left _
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "do not depend on the junk values of `deriv`" (since := "2026-05-13")]
 theorem deriv_zero : deriv 0 = id :=
   deriv_eq_id_of_nfp_eq_id nfp_zero
 
+set_option linter.deprecated false in
+@[deprecated "do not depend on the junk values of `deriv`" (since := "2026-05-13")]
 theorem deriv_zero_left (a) : deriv 0 a = a := by
   rw [deriv_zero, id_eq]
 
@@ -468,10 +475,9 @@ theorem nfp_mul_zero (a : Ordinal) : nfp (a * ·) 0 = 0 := by
 
 theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) :
     nfp (a * ·) b = a ^ ω := by
-  rcases eq_zero_or_pos a with ha | ha
-  · rw [ha, zero_opow omega0_ne_zero] at hba ⊢
-    simp_rw [nonpos_iff_eq_zero.1 hba, zero_mul]
-    exact nfp_zero_left 0
+  rcases eq_zero_or_pos a with rfl | ha
+  · rw [zero_opow omega0_ne_zero] at hba
+    cases hba.not_gt hb
   apply le_antisymm
   · apply nfp_le_fp (isNormal_mul_right ha).monotone hba
     rw [← opow_one_add, one_add_omega0]

Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

@@ -75,7 +75,7 @@ protected theorem id (ho : o ≤ o.cof.ord) : IsFundamentalSeq (o := o) id where
 protected theorem zero (f : Iio 0 → Iio 0) : IsFundamentalSeq f where
   strictMono _ := by simp
   le_ord_cof := by simp
-  isCofinal_range := .of_isEmpty _
+  isCofinal_range := .of_isEmpty
 
 /-- The length one sequence `(o)` is a fundamental sequence for `o + 1`. -/
 protected theorem add_one (o : Ordinal) :