feat(set_theory/ordinal/arithmetic): miscellaneous arithmetic lemmas (#15990)

vihdzp · vihdzp · commit b67044ba53af · 2023-03-26T17:00:46.000Z
Will be used to prove statements about the Cantor Normal Form.
diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean
@@ -479,7 +479,7 @@ protected theorem sub_eq_zero_iff_le {a b : ordinal} : a - b = 0 ↔ a ≤ b :=
 theorem sub_sub (a b c : ordinal) : a - b - c = a - (b + c) :=
 eq_of_forall_ge_iff $ λ d, by rw [sub_le, sub_le, sub_le, add_assoc]
 
-theorem add_sub_add_cancel (a b c : ordinal) : a + b - (a + c) = b - c :=
+@[simp] theorem add_sub_add_cancel (a b c : ordinal) : a + b - (a + c) = b - c :=
 by rw [← sub_sub, add_sub_cancel]
 
 theorem sub_is_limit {a b} (l : is_limit a) (h : b < a) : is_limit (a - b) :=
@@ -804,6 +804,8 @@ instance : has_mod ordinal := ⟨λ a b, a - b * (a / b)⟩
 
 theorem mod_def (a b : ordinal) : a % b = a - b * (a / b) := rfl
 
+theorem mod_le (a b : ordinal) : a % b ≤ a := sub_le_self a _
+
 @[simp] theorem mod_zero (a : ordinal) : a % 0 = a :=
 by simp only [mod_def, div_zero, zero_mul, sub_zero]
 
@@ -841,6 +843,24 @@ end
 theorem dvd_iff_mod_eq_zero {a b : ordinal} : b ∣ a ↔ a % b = 0 :=
 ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
 
+@[simp] theorem mul_add_mod_self (x y z : ordinal) : (x * y + z) % x = z % x :=
+begin
+  rcases eq_or_ne x 0 with rfl | hx,
+  { simp },
+  { rwa [mod_def, mul_add_div, mul_add, ←sub_sub, add_sub_cancel, mod_def] }
+end
+
+@[simp] theorem mul_mod (x y : ordinal) : x * y % x = 0 := by simpa using mul_add_mod_self x y 0
+
+theorem mod_mod_of_dvd (a : ordinal) {b c : ordinal} (h : c ∣ b) : a % b % c = a % c :=
+begin
+  nth_rewrite_rhs 0 ←div_add_mod a b,
+  rcases h with ⟨d, rfl⟩,
+  rw [mul_assoc, mul_add_mod_self]
+end
+
+@[simp] theorem mod_mod (a b : ordinal) : a % b % b = a % b := mod_mod_of_dvd a dvd_rfl
+
 /-! ### Families of ordinals
 
 There are two kinds of indexed families that naturally arise when dealing with ordinals: those
diff --git a/src/set_theory/ordinal/exponential.lean b/src/set_theory/ordinal/exponential.lean
@@ -190,12 +190,10 @@ end
 theorem opow_one_add (a b : ordinal) : a ^ (1 + b) = a * a ^ b :=
 by rw [opow_add, opow_one]
 
-theorem opow_dvd_opow (a) {b c : ordinal}
-  (h : b ≤ c) : a ^ b ∣ a ^ c :=
-by { rw [← ordinal.add_sub_cancel_of_le h, opow_add], apply dvd_mul_right }
+theorem opow_dvd_opow (a) {b c : ordinal} (h : b ≤ c) : a ^ b ∣ a ^ c :=
+⟨a ^ (c - b), by rw [←opow_add, ordinal.add_sub_cancel_of_le h] ⟩
 
-theorem opow_dvd_opow_iff {a b c : ordinal}
-  (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c :=
+theorem opow_dvd_opow_iff {a b c : ordinal} (a1 : 1 < a) : a ^ b ∣ a ^ c ↔ b ≤ c :=
 ⟨λ h, le_of_not_lt $ λ hn,
   not_le_of_lt ((opow_lt_opow_iff_right a1).2 hn) $
     le_of_dvd (opow_ne_zero _ $ one_le_iff_ne_zero.1 $ a1.le) h,
@@ -385,6 +383,14 @@ begin
   rw [add_zero, mul_one]
 end
 
+theorem div_opow_log_pos (b : ordinal) {o : ordinal} (ho : o ≠ 0) : 0 < o / b ^ log b o :=
+begin
+  rcases eq_zero_or_pos b with (rfl | hb),
+  { simpa using ordinal.pos_iff_ne_zero.2 ho },
+  { rw div_pos (opow_ne_zero _ hb.ne'),
+    exact opow_log_le_self b ho }
+end
+
 theorem div_opow_log_lt {b : ordinal} (o : ordinal) (hb : 1 < b) : o / b ^ log b o < b :=
 begin
   rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ←opow_succ],
diff --git a/src/set_theory/ordinal/notation.lean b/src/set_theory/ordinal/notation.lean
@@ -428,7 +428,7 @@ instance sub_NF (o₁ o₂) : ∀ [NF o₁] [NF o₂], NF (o₁ - o₂)
   { change e₁ = e₂ at ee, substI e₂, unfold sub._match_1,
     cases mn : (n₁:ℕ) - n₂; dsimp only [sub._match_2],
     { by_cases en : n₁ = n₂,
-      { simp [en], rwa [add_sub_add_cancel] },
+      { simpa [en] },
       { simp [en, -repr],
         exact (ordinal.sub_eq_zero_iff_le.2 $ le_of_lt $ oadd_lt_oadd_2 h₁ $
           lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt pnat.eq en)).symm } },
