chore(set_theory/ordinal/arithmetic): review cast API (#14757)

This PR does the following:
- swap the direction of `nat_cast_succ` to match `nat.cast_succ`.
- make various arguments explicit.
- remove `lift_type_fin`, as it's a trivial consequence of `type_fin` and `lift_nat_cast`.
- tag various theorems as `norm_cast`.
- golf or otherwise cleanup various proofs.

src/set_theory/cardinal/cofinality.lean

@@ -596,7 +596,7 @@ begin
     rw [e, ord_nat] at this,
     cases n,
     { simp at e, simpa [e, not_zero_is_limit] using l },
-    { rw [← nat_cast_succ, cof_succ] at this,
+    { rw [nat_cast_succ, cof_succ] at this,
       rw [← this, cof_eq_one_iff_is_succ] at e,
       rcases e with ⟨a, rfl⟩,
       exact not_succ_is_limit _ l } }

src/set_theory/ordinal/arithmetic.lean

@@ -115,7 +115,7 @@ ne_of_gt $ succ_pos o
 @[simp] theorem card_succ (o : ordinal) : card (succ o) = card o + 1 :=
 by simp only [←add_one_eq_succ, card_add, card_one]
 
-theorem nat_cast_succ (n : ℕ) : (succ n : ordinal) = n.succ := rfl
+theorem nat_cast_succ (n : ℕ) : ↑n.succ = succ (n : ordinal) := rfl
 
 theorem add_left_cancel (a) {b c : ordinal} : a + b = a + c ↔ b = c :=
 by simp only [le_antisymm_iff, add_le_add_iff_left]
@@ -136,9 +136,9 @@ instance add_swap_contravariant_class_lt :
   contravariant_class ordinal.{u} ordinal.{u} (swap (+)) (<) :=
 ⟨λ a b c, lt_imp_lt_of_le_imp_le (λ h, add_le_add_right h _)⟩
 
-theorem add_le_add_iff_right {a b : ordinal} (n : ℕ) : a + n ≤ b + n ↔ a ≤ b :=
-by induction n with n ih; [rw [nat.cast_zero, add_zero, add_zero],
-  rw [← nat_cast_succ, add_succ, add_succ, succ_le_succ_iff, ih]]
+theorem add_le_add_iff_right {a b : ordinal} : ∀ n : ℕ, a + n ≤ b + n ↔ a ≤ b
+| 0     := by simp
+| (n+1) := by rw [nat_cast_succ, add_succ, add_succ, succ_le_succ_iff, add_le_add_iff_right]
 
 theorem add_right_cancel {a b : ordinal} (n : ℕ) : a + n = b + n ↔ a = b :=
 by simp only [le_antisymm_iff, add_le_add_iff_right]
@@ -2113,56 +2113,59 @@ end
 
 /-! ### Casting naturals into ordinals, compatibility with operations -/
 
-@[simp] theorem nat_cast_mul {m n : ℕ} : ((m * n : ℕ) : ordinal) = m * n :=
-by induction n with n IH; [simp only [nat.cast_zero, nat.mul_zero, mul_zero],
-  rw [nat.mul_succ, nat.cast_add, IH, nat.cast_succ, mul_add_one]]
+@[simp, norm_cast] theorem nat_cast_mul (m : ℕ) : ∀ n : ℕ, ((m * n : ℕ) : ordinal) = m * n
+| 0     := by simp
+| (n+1) := by rw [nat.mul_succ, nat.cast_add, nat_cast_mul, nat.cast_succ, mul_add_one]
 
-@[simp] theorem nat_cast_opow {m n : ℕ} : ((pow m n : ℕ) : ordinal) = m ^ n :=
-by induction n with n IH; [simp only [pow_zero, nat.cast_zero, opow_zero, nat.cast_one],
-  rw [pow_succ', nat_cast_mul, IH, nat.cast_succ, add_one_eq_succ, opow_succ]]
+@[simp, norm_cast] theorem nat_cast_opow (m : ℕ) : ∀ n : ℕ, ((pow m n : ℕ) : ordinal) = m ^ n
+| 0     := by simp
+| (n+1) := by rw [pow_succ', nat_cast_mul, nat_cast_opow, nat.cast_succ, add_one_eq_succ, opow_succ]
 
-@[simp] theorem nat_cast_le {m n : ℕ} : (m : ordinal) ≤ n ↔ m ≤ n :=
-by rw [← cardinal.ord_nat, ← cardinal.ord_nat,
-       cardinal.ord_le_ord, cardinal.nat_cast_le]
+@[simp, norm_cast] theorem nat_cast_le {m n : ℕ} : (m : ordinal) ≤ n ↔ m ≤ n :=
+by rw [←cardinal.ord_nat, ←cardinal.ord_nat, cardinal.ord_le_ord, cardinal.nat_cast_le]
 
-@[simp] theorem nat_cast_lt {m n : ℕ} : (m : ordinal) < n ↔ m < n :=
+@[simp, norm_cast] theorem nat_cast_lt {m n : ℕ} : (m : ordinal) < n ↔ m < n :=
 by simp only [lt_iff_le_not_le, nat_cast_le]
 
-@[simp] theorem nat_cast_inj {m n : ℕ} : (m : ordinal) = n ↔ m = n :=
+@[simp, norm_cast] theorem nat_cast_inj {m n : ℕ} : (m : ordinal) = n ↔ m = n :=
 by simp only [le_antisymm_iff, nat_cast_le]
 
-@[simp] theorem nat_cast_eq_zero {n : ℕ} : (n : ordinal) = 0 ↔ n = 0 :=
+@[simp, norm_cast] theorem nat_cast_eq_zero {n : ℕ} : (n : ordinal) = 0 ↔ n = 0 :=
 @nat_cast_inj n 0
 
 theorem nat_cast_ne_zero {n : ℕ} : (n : ordinal) ≠ 0 ↔ n ≠ 0 :=
 not_congr nat_cast_eq_zero
 
-@[simp] theorem nat_cast_pos {n : ℕ} : (0 : ordinal) < n ↔ 0 < n :=
+@[simp, norm_cast] theorem nat_cast_pos {n : ℕ} : (0 : ordinal) < n ↔ 0 < n :=
 @nat_cast_lt 0 n
 
-@[simp] theorem nat_cast_sub {m n : ℕ} : ((m - n : ℕ) : ordinal) = m - n :=
-(_root_.le_total m n).elim
-  (λ h, by rw [tsub_eq_zero_iff_le.2 h, ordinal.sub_eq_zero_iff_le.2 (nat_cast_le.2 h)]; refl)
-  (λ h, (add_left_cancel n).1 $ by rw [← nat.cast_add,
-     add_tsub_cancel_of_le h, ordinal.add_sub_cancel_of_le (nat_cast_le.2 h)])
+@[simp, norm_cast] theorem nat_cast_sub (m n : ℕ) : ((m - n : ℕ) : ordinal) = m - n :=
+begin
+  cases le_total m n with h h,
+  { rw [tsub_eq_zero_iff_le.2 h, ordinal.sub_eq_zero_iff_le.2 (nat_cast_le.2 h)],
+    refl },
+  { apply (add_left_cancel n).1,
+    rw [←nat.cast_add, add_tsub_cancel_of_le h, ordinal.add_sub_cancel_of_le (nat_cast_le.2 h)] }
+end
 
-@[simp] theorem nat_cast_div {m n : ℕ} : ((m / n : ℕ) : ordinal) = m / n :=
-if n0 : n = 0 then by simp only [n0, nat.div_zero, nat.cast_zero, div_zero] else
-have n0':_, from nat_cast_ne_zero.2 n0,
-le_antisymm
-  (by rw [le_div n0', ← nat_cast_mul, nat_cast_le, mul_comm];
-      apply nat.div_mul_le_self)
-  (by rw [div_le n0', ←add_one_eq_succ, ← nat.cast_succ, ← nat_cast_mul,
-          nat_cast_lt, mul_comm, ← nat.div_lt_iff_lt_mul (nat.pos_of_ne_zero n0)];
-      apply nat.lt_succ_self)
+@[simp, norm_cast] theorem nat_cast_div (m n : ℕ) : ((m / n : ℕ) : ordinal) = m / n :=
+begin
+  rcases eq_or_ne n 0 with rfl | hn,
+  { simp },
+  { have hn' := nat_cast_ne_zero.2 hn,
+    apply le_antisymm,
+    { rw [le_div hn', ←nat_cast_mul, nat_cast_le, mul_comm],
+      apply nat.div_mul_le_self },
+    { rw [div_le hn', ←add_one_eq_succ, ←nat.cast_succ, ←nat_cast_mul, nat_cast_lt, mul_comm,
+        ←nat.div_lt_iff_lt_mul (nat.pos_of_ne_zero hn)],
+      apply nat.lt_succ_self } }
+end
 
-@[simp] theorem nat_cast_mod {m n : ℕ} : ((m % n : ℕ) : ordinal) = m % n :=
-by rw [← add_left_cancel (n*(m/n)), div_add_mod, ← nat_cast_div, ← nat_cast_mul, ← nat.cast_add,
-       nat.div_add_mod]
+@[simp, norm_cast] theorem nat_cast_mod (m n : ℕ) : ((m % n : ℕ) : ordinal) = m % n :=
+by rw [←add_left_cancel, div_add_mod, ←nat_cast_div, ←nat_cast_mul, ←nat.cast_add, nat.div_add_mod]
 
 @[simp] theorem nat_le_card {o} {n : ℕ} : (n : cardinal) ≤ card o ↔ (n : ordinal) ≤ o :=
-⟨λ h, by rwa [← cardinal.ord_le, cardinal.ord_nat] at h,
- λ h, card_nat n ▸ card_le_card h⟩
+⟨λ h, by rwa [←cardinal.ord_le, cardinal.ord_nat] at h, λ h, card_nat n ▸ card_le_card h⟩
 
 @[simp] theorem nat_lt_card {o} {n : ℕ} : (n : cardinal) < card o ↔ (n : ordinal) < o :=
 by { rw [←succ_le_iff, ←succ_le_iff, ←nat_succ, nat_le_card], refl }
@@ -2177,17 +2180,14 @@ le_iff_le_iff_lt_iff_lt.2 nat_lt_card
 by simp only [le_antisymm_iff, card_le_nat, nat_le_card]
 
 @[simp] theorem type_fin (n : ℕ) : @type (fin n) (<) _ = n :=
-by rw [← card_eq_nat, card_type, mk_fin]
-
-@[simp] theorem lift_nat_cast (n : ℕ) : lift n = n :=
-by induction n with n ih; [simp only [nat.cast_zero, lift_zero],
-  simp only [nat.cast_succ, lift_add, ih, lift_one]]
+by rw [←card_eq_nat, card_type, mk_fin]
 
-theorem lift_type_fin (n : ℕ) : lift (@type (fin n) (<) _) = n :=
-by simp only [type_fin, lift_nat_cast]
+@[simp] theorem lift_nat_cast : ∀ n : ℕ, lift.{u v} n = n
+| 0     := by simp
+| (n+1) := by simp [lift_nat_cast n]
 
 theorem type_fintype (r : α → α → Prop) [is_well_order α r] [fintype α] : type r = fintype.card α :=
-by rw [← card_eq_nat, card_type, mk_fintype]
+by rw [←card_eq_nat, card_type, mk_fintype]
 
 end ordinal
 

src/set_theory/ordinal/notation.lean

@@ -495,7 +495,7 @@ instance mul_NF : ∀ o₁ o₂ [NF o₁] [NF o₂], NF (o₁ * o₂)
   by_cases e0 : e₂ = 0; simp [e0, mul],
   { cases nat.exists_eq_succ_of_ne_zero n₂.ne_zero with x xe,
     simp [h₂.zero_of_zero e0, xe, -nat.cast_succ],
-    rw [← nat_cast_succ x, add_mul_succ _ ao, mul_assoc] },
+    rw [nat_cast_succ x, add_mul_succ _ ao, mul_assoc] },
   { haveI := h₁.fst, haveI := h₂.fst,
     simp [IH, repr_add, opow_add, mul_add],
     rw ← mul_assoc, congr' 2,
@@ -740,7 +740,7 @@ begin
         ω0 ^ k.succ * α' + R'
       = ω0 ^ succ k * α' + (ω0 ^ k * α' * m + R) : by rw [nat_cast_succ, RR, ← mul_assoc]
   ... = (ω0 ^ k * α' + R) * α' + (ω0 ^ k * α' + R) * m : _
-  ... = (α' + m) ^ succ k.succ : by rw [← mul_add, ← nat_cast_succ, opow_succ, IH.2],
+  ... = (α' + m) ^ succ k.succ : by rw [← mul_add, nat_cast_succ, opow_succ, IH.2],
   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,
@@ -755,7 +755,7 @@ begin
       rw opow_mul, simpa [-opow_succ] } },
   { cases m,
     { have : R = 0, {cases k; simp [R, opow_aux]}, simp [this] },
-    { rw [← nat_cast_succ, add_mul_succ],
+    { rw [nat_cast_succ, add_mul_succ],
       apply add_absorp Rl,
       rw [opow_mul, opow_succ],
       apply mul_le_mul_left',
@@ -873,13 +873,13 @@ begin
     { have := opow_pos _ omega_pos,
       refine ⟨mul_is_limit this omega_is_limit,
         λ i, ⟨this, _, λ H, @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega'⟩,
-      rw [← mul_succ, nat_cast_succ, ordinal.mul_lt_mul_iff_left this],
+      rw [← mul_succ, ← nat_cast_succ, ordinal.mul_lt_mul_iff_left this],
       apply nat_lt_omega },
     { have := opow_pos _ omega_pos,
       refine ⟨
         add_is_limit _ (mul_is_limit this omega_is_limit), λ i, ⟨this, _, _⟩,
         exists_lt_add exists_lt_mul_omega'⟩,
-      { rw [← mul_succ, nat_cast_succ, ordinal.mul_lt_mul_iff_left this],
+      { rw [← mul_succ, ← nat_cast_succ, ordinal.mul_lt_mul_iff_left this],
         apply nat_lt_omega },
       { refine λ H, H.fst.oadd _ (NF.below_of_lt' _ (@NF.oadd_zero _ _ (iha.2 H.fst))),
         rw [repr, repr, add_zero, iha.1, opow_succ, ordinal.mul_lt_mul_iff_left this],