chore(set_theory/ordinal/arithmetic): change 0 < x assumptions to `…

…x ≠ 0` (#15562)

Converting from `h : 0 < x` to `h : x ≠ 0` is as easy as `h.ne'`, while the other way round requires `ordinal.pos_iff_ne_zero.2 h`. As such, we prefer the latter form throughout the ordinal logarithm API.

We also rename hypotheses like `b0` and `x0` to more standard names like `hb` and `hx`.

src/set_theory/ordinal/arithmetic.lean

@@ -2006,14 +2006,14 @@ if h : 1 < b then pred (Inf {o | x < b ^ o}) else 0
 theorem log_nonempty {b x : ordinal} (h : 1 < b) : {o | x < b ^ o}.nonempty :=
 ⟨_, succ_le_iff.1 (right_le_opow _ h)⟩
 
-theorem log_def {b : ordinal} (b1 : 1 < b) (x : ordinal) : log b x = pred (Inf {o | x < b ^ o}) :=
-by simp only [log, dif_pos b1]
+theorem log_def {b : ordinal} (h : 1 < b) (x : ordinal) : log b x = pred (Inf {o | x < b ^ o}) :=
+by simp only [log, dif_pos h]
 
-theorem log_of_not_one_lt_left {b : ordinal} (b1 : ¬ 1 < b) (x : ordinal) : log b x = 0 :=
-by simp only [log, dif_neg b1]
+theorem log_of_not_one_lt_left {b : ordinal} (h : ¬ 1 < b) (x : ordinal) : log b x = 0 :=
+by simp only [log, dif_neg h]
 
-theorem log_of_left_le_one {b : ordinal} (b1 : b ≤ 1) : ∀ x, log b x = 0 :=
-log_of_not_one_lt_left b1.not_lt
+theorem log_of_left_le_one {b : ordinal} (h : b ≤ 1) : ∀ x, log b x = 0 :=
+log_of_not_one_lt_left h.not_lt
 
 @[simp] lemma log_zero_left : ∀ b, log 0 b = 0 :=
 log_of_left_le_one zero_le_one
@@ -2031,55 +2031,56 @@ else by simp only [log_of_not_one_lt_left b1]
 @[simp] theorem log_one_left : ∀ b, log 1 b = 0 :=
 log_of_left_le_one le_rfl
 
-theorem succ_log_def {b x : ordinal} (b1 : 1 < b) (x0 : 0 < x) :
+theorem succ_log_def {b x : ordinal} (hb : 1 < b) (hx : x ≠ 0) :
   succ (log b x) = Inf {o | x < b ^ o} :=
 begin
   let t := Inf {o | x < b ^ o},
-  have : x < b ^ t := Inf_mem (log_nonempty b1),
+  have : x < b ^ t := Inf_mem (log_nonempty hb),
   rcases zero_or_succ_or_limit t with h|h|h,
-  { refine ((one_le_iff_pos.2 x0).not_lt _).elim,
+  { refine ((one_le_iff_ne_zero.2 hx).not_lt _).elim,
     simpa only [h, opow_zero] },
-  { rw [show log b x = pred t, from log_def b1 x,
+  { rw [show log b x = pred t, from log_def hb x,
         succ_pred_iff_is_succ.2 h] },
-  { rcases (lt_opow_of_limit (zero_lt_one.trans b1).ne' h).1 this with ⟨a, h₁, h₂⟩,
-    exact h₁.not_le.elim ((le_cInf_iff'' (log_nonempty b1)).1 le_rfl a h₂) }
+  { rcases (lt_opow_of_limit (zero_lt_one.trans hb).ne' h).1 this with ⟨a, h₁, h₂⟩,
+    exact h₁.not_le.elim ((le_cInf_iff'' (log_nonempty hb)).1 le_rfl a h₂) }
 end
 
-theorem lt_opow_succ_log_self {b : ordinal} (b1 : 1 < b) (x : ordinal) : x < b ^ succ (log b x) :=
+theorem lt_opow_succ_log_self {b : ordinal} (hb : 1 < b) (x : ordinal) : x < b ^ succ (log b x) :=
 begin
-  cases lt_or_eq_of_le (ordinal.zero_le x) with x0 x0,
-  { rw [succ_log_def b1 x0], exact Inf_mem (log_nonempty b1) },
-  { subst x, apply opow_pos _ (zero_lt_one.trans b1) }
+  rcases eq_or_ne x 0 with rfl | hx,
+  { apply opow_pos _ (zero_lt_one.trans hb) },
+  { rw succ_log_def hb hx,
+    exact Inf_mem (log_nonempty hb) }
 end
 
-theorem opow_log_le_self (b) {x : ordinal} (x0 : 0 < x) : b ^ log b x ≤ x :=
+theorem opow_log_le_self (b) {x : ordinal} (hx : x ≠ 0) : b ^ log b x ≤ x :=
 begin
   rcases eq_or_ne b 0 with rfl | b0,
   { rw zero_opow',
-    refine (sub_le_self _ _).trans (one_le_iff_pos.2 x0) },
-  cases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with b1 b1,
+    refine (sub_le_self _ _).trans (one_le_iff_ne_zero.2 hx) },
+  rcases lt_or_eq_of_le (one_le_iff_ne_zero.2 b0) with hb | rfl,
   { refine le_of_not_lt (λ h, (lt_succ (log b x)).not_le _),
     have := @cInf_le' _ _ {o | x < b ^ o} _ h,
-    rwa ←succ_log_def b1 x0 at this },
-  { rw [←b1, one_opow], exact one_le_iff_pos.2 x0 }
+    rwa ←succ_log_def hb hx at this },
+  { rwa [one_opow, one_le_iff_ne_zero] }
 end
 
 /-- `opow b` and `log b` (almost) form a Galois connection. -/
-theorem opow_le_iff_le_log {b x c : ordinal} (b1 : 1 < b) (x0 : 0 < x) : b ^ c ≤ x ↔ c ≤ log b x :=
+theorem opow_le_iff_le_log {b x c : ordinal} (hb : 1 < b) (hx : x ≠ 0) : b ^ c ≤ x ↔ c ≤ log b x :=
 ⟨λ h, le_of_not_lt $ λ hn,
-   (lt_opow_succ_log_self b1 x).not_le $
-   ((opow_le_opow_iff_right b1).2 (succ_le_of_lt hn)).trans h,
-λ h, ((opow_le_opow_iff_right b1).2 h).trans (opow_log_le_self b x0)⟩
+   (lt_opow_succ_log_self hb x).not_le $
+   ((opow_le_opow_iff_right hb).2 (succ_le_of_lt hn)).trans h,
+λ h, ((opow_le_opow_iff_right hb).2 h).trans (opow_log_le_self b hx)⟩
 
-theorem lt_opow_iff_log_lt {b x c : ordinal} (b1 : 1 < b) (x0 : 0 < x) : x < b ^ c ↔ log b x < c :=
-lt_iff_lt_of_le_iff_le (opow_le_iff_le_log b1 x0)
+theorem lt_opow_iff_log_lt {b x c : ordinal} (hb : 1 < b) (hx : x ≠ 0) : x < b ^ c ↔ log b x < c :=
+lt_iff_lt_of_le_iff_le (opow_le_iff_le_log hb hx)
 
-theorem log_pos {b o : ordinal} (hb : 1 < b) (ho : 0 < o) (hbo : b ≤ o) : 0 < log b o :=
+theorem log_pos {b o : ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) : 0 < log b o :=
 by rwa [←succ_le_iff, succ_zero, ←opow_le_iff_le_log hb ho, opow_one]
 
 theorem log_eq_zero {b o : ordinal} (hbo : o < b) : log b o = 0 :=
 begin
-  rcases eq_zero_or_pos o with rfl | ho,
+  rcases eq_or_ne o 0 with rfl | ho,
   { exact log_zero_right b },
   cases le_or_lt b 1 with hb hb,
   { rcases le_one_iff.1 hb with rfl | rfl,
@@ -2089,27 +2090,27 @@ begin
 end
 
 @[mono] theorem log_mono_right (b) {x y : ordinal} (xy : x ≤ y) : log b x ≤ log b y :=
-if x0 : x = 0 then by simp only [x0, log_zero_right, ordinal.zero_le] else
-have x0 : 0 < x, from ordinal.pos_iff_ne_zero.2 x0,
-if b1 : 1 < b then
-  (opow_le_iff_le_log b1 (lt_of_lt_of_le x0 xy)).1 $ (opow_log_le_self _ x0).trans xy
-else by simp only [log_of_not_one_lt_left b1, ordinal.zero_le]
+if hx : x = 0 then by simp only [hx, log_zero_right, ordinal.zero_le] else
+if hb : 1 < b then
+  (opow_le_iff_le_log hb (lt_of_lt_of_le (ordinal.pos_iff_ne_zero.2 hx) xy).ne').1 $
+    (opow_log_le_self _ hx).trans xy
+else by simp only [log_of_not_one_lt_left hb, ordinal.zero_le]
 
 theorem log_le_self (b x : ordinal) : log b x ≤ x :=
-if x0 : x = 0 then by simp only [x0, log_zero_right, ordinal.zero_le] else
-if b1 : 1 < b then (right_le_opow _ b1).trans (opow_log_le_self b (ordinal.pos_iff_ne_zero.2 x0))
-else by simp only [log_of_not_one_lt_left b1, ordinal.zero_le]
+if hx : x = 0 then by simp only [hx, log_zero_right, ordinal.zero_le] else
+if hb : 1 < b then (right_le_opow _ hb).trans (opow_log_le_self b hx)
+else by simp only [log_of_not_one_lt_left hb, ordinal.zero_le]
 
 @[simp] theorem log_one_right (b : ordinal) : log b 1 = 0 :=
 if hb : 1 < b then log_eq_zero hb else log_of_not_one_lt_left hb 1
 
-theorem mod_opow_log_lt_self {b o : ordinal} (b0 : b ≠ 0) (o0 : o ≠ 0) : o % b ^ log b o < o :=
-(mod_lt _ $ opow_ne_zero _ b0).trans_le (opow_log_le_self _ $ ordinal.pos_iff_ne_zero.2 o0)
+theorem mod_opow_log_lt_self {b o : ordinal} (hb : b ≠ 0) (ho : o ≠ 0) : o % b ^ log b o < o :=
+(mod_lt _ $ opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)
 
-theorem log_mod_opow_log_lt_log_self {b o : ordinal} (hb : 1 < b) (ho : 0 < o) (hbo : b ≤ o) :
+theorem log_mod_opow_log_lt_log_self {b o : ordinal} (hb : 1 < b) (ho : o ≠ 0) (hbo : b ≤ o) :
   log b (o % b ^ log b o) < log b o :=
 begin
-  cases eq_zero_or_pos (o % b ^ log b o),
+  cases eq_or_ne (o % b ^ log b o) 0,
   { rw [h, log_zero_right],
     apply log_pos hb ho hbo },
   { rw [←succ_le_iff, succ_log_def hb h],
@@ -2119,8 +2120,9 @@ begin
     exact opow_pos _ (zero_lt_one.trans hb) }
 end
 
-lemma opow_mul_add_pos {b v : ordinal} (hb : 0 < b) (u) (hv : 0 < v) (w) : 0 < b ^ u * v + w :=
-(opow_pos u hb).trans_le ((le_mul_left _ hv).trans (le_add_right _ _))
+lemma opow_mul_add_pos {b v : ordinal} (hb : b ≠ 0) (u) (hv : v ≠ 0) (w) : 0 < b ^ u * v + w :=
+(opow_pos u $ ordinal.pos_iff_ne_zero.2 hb).trans_le $
+  (le_mul_left _ $ ordinal.pos_iff_ne_zero.2 hv).trans $ le_add_right _ _
 
 lemma opow_mul_add_lt_opow_mul_succ {b u w : ordinal} (v : ordinal) (hw : w < b ^ u) :
   b ^ u * v + w < b ^ u * (succ v) :=
@@ -2133,22 +2135,22 @@ begin
   exact opow_succ b u
 end
 
-theorem log_opow_mul_add {b u v w : ordinal} (hb : 1 < b) (hv : 0 < v) (hvb : v < b)
+theorem log_opow_mul_add {b u v w : ordinal} (hb : 1 < b) (hv : v ≠ 0) (hvb : v < b)
   (hw : w < b ^ u) : log b (b ^ u * v + w) = u :=
 begin
-  have hpos := opow_mul_add_pos (zero_lt_one.trans hb) u hv w,
+  have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne',
   by_contra' hne,
   cases lt_or_gt_of_ne hne with h h,
-  { rw ←lt_opow_iff_log_lt hb hpos at h,
-    exact h.not_le ((le_mul_left _ hv).trans (le_add_right _ _)) },
+  { rw ←lt_opow_iff_log_lt hb hne' at h,
+    exact h.not_le ((le_mul_left _ (ordinal.pos_iff_ne_zero.2 hv)).trans (le_add_right _ _)) },
   { change _ < _ at h,
-    rw [←succ_le_iff, ←opow_le_iff_le_log hb hpos] at h,
+    rw [←succ_le_iff, ←opow_le_iff_le_log hb hne'] at h,
     exact (not_lt_of_le h) (opow_mul_add_lt_opow_succ hvb hw) }
 end
 
 theorem log_opow {b : ordinal} (hb : 1 < b) (x : ordinal) : log b (b ^ x) = x :=
 begin
-  convert log_opow_mul_add hb zero_lt_one hb (opow_pos x (zero_lt_one.trans hb)),
+  convert log_opow_mul_add hb zero_ne_one.symm hb (opow_pos x (zero_lt_one.trans hb)),
   rw [add_zero, mul_one]
 end
 
@@ -2158,12 +2160,12 @@ begin
   exact lt_opow_succ_log_self hb o
 end
 
-theorem add_log_le_log_mul {x y : ordinal} (b : ordinal) (x0 : 0 < x) (y0 : 0 < y) :
+theorem add_log_le_log_mul {x y : ordinal} (b : ordinal) (hx : x ≠ 0) (hy : y ≠ 0) :
   log b x + log b y ≤ log b (x * y) :=
 begin
   by_cases hb : 1 < b,
-  { rw [←opow_le_iff_le_log hb (mul_pos x0 y0), opow_add],
-    exact mul_le_mul' (opow_log_le_self b x0) (opow_log_le_self b y0) },
+  { rw [←opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add],
+    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy) },
   simp only [log_of_not_one_lt_left hb, zero_add]
 end
 

src/set_theory/ordinal/cantor_normal_form.lean

@@ -98,7 +98,7 @@ begin
     refine ⟨⟨le_rfl, λ p m, _⟩, λ p m, _⟩,
     { exact (IH₁ p m).trans (log_mono_right _ $ le_of_lt $ mod_opow_log_lt_self hb ho) },
     { refine (IH₁ p m).trans_lt ((lt_opow_iff_log_lt hb' _).1 _),
-      { rw ordinal.pos_iff_ne_zero, intro e,
+      { intro e,
         rw e at m, simpa only [CNF_zero] using m },
       { exact mod_lt _ (opow_ne_zero _ hb) } } },
   { by_cases ho : o = 0,
@@ -132,8 +132,7 @@ begin
   simp only [CNF_ne_zero hb ho, list.mem_cons_iff, forall_eq_or_imp, iff_true_intro @IH, and_true],
   nth_rewrite 1 ←@succ_le_iff,
   rw [div_lt (opow_ne_zero _ hb), ←opow_succ, le_div (opow_ne_zero _ hb), succ_zero, mul_one],
-  refine ⟨lt_opow_succ_log_self hb' _, opow_log_le_self _ _⟩,
-  rwa ordinal.pos_iff_ne_zero
+  exact ⟨lt_opow_succ_log_self hb' _, opow_log_le_self _ ho⟩
 end
 
 /-- Every coefficient in the Cantor normal form `CNF b o` is less than `b`. -/

src/set_theory/ordinal/principal.lean

@@ -211,7 +211,7 @@ begin
   { simp only [principal_zero, or.inl] },
   { rw [principal_add_iff_add_left_eq_self],
     simp only [ho, false_or],
-    refine ⟨λ H, ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ (ordinal.pos_iff_ne_zero.2 ho)))
+    refine ⟨λ H, ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ ho))
         .resolve_left $ λ h, _).symm⟩, λ ⟨b, e⟩, e.symm ▸ λ a, add_omega_opow⟩,
     have := H _ h,
     have := lt_opow_succ_log_self one_lt_omega o,
@@ -389,12 +389,12 @@ theorem mul_omega_dvd {a : ordinal}
   (a0 : 0 < a) (ha : a < omega) : ∀ {b}, omega ∣ b → a * b = b
 | _ ⟨b, rfl⟩ := by rw [← mul_assoc, mul_omega a0 ha]
 
-theorem mul_eq_opow_log_succ {a b : ordinal.{u}} (ha : 0 < a) (hb : principal (*) b) (hb₂ : 2 < b) :
+theorem mul_eq_opow_log_succ {a b : ordinal.{u}} (ha : a ≠ 0) (hb : principal (*) b) (hb₂ : 2 < b) :
   a * b = b ^ succ (log b a) :=
 begin
   apply le_antisymm,
   { have hbl := principal_mul_is_limit hb₂ hb,
-    rw [←is_normal.bsup_eq.{u u} (mul_is_normal ha) hbl, bsup_le_iff],
+    rw [←is_normal.bsup_eq.{u u} (mul_is_normal (ordinal.pos_iff_ne_zero.2 ha)) hbl, bsup_le_iff],
     intros c hcb,
     have hb₁ : 1 < b := (lt_succ 1).trans hb₂,
     have hbo₀ : b ^ b.log a ≠ 0 := ordinal.pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁)),