feat(set_theory/ordinal/arithmetic): tweak type_add and type_mul (#…

…15193)

This renames `type_mul` to the more accurate `type_prod_lex`, and renames `type_add` to `type_sum_lex` and reverses the order of the equality so that the two lemmas match.

src/set_theory/ordinal/arithmetic.lean

@@ -191,7 +191,7 @@ end
 
 theorem add_eq_zero_iff {a b : ordinal} : a + b = 0 ↔ (a = 0 ∧ b = 0) :=
 induction_on a $ λ α r _, induction_on b $ λ β s _, begin
-  simp_rw [type_add, type_eq_zero_iff_is_empty],
+  simp_rw [←type_sum_lex, type_eq_zero_iff_is_empty],
   exact is_empty_sum
 end
 
@@ -550,7 +550,7 @@ theorem sub_is_limit {a b} (l : is_limit a) (h : b < a) : is_limit (a - b) :=
 @[simp] theorem one_add_omega : 1 + ω = ω :=
 begin
   refine le_antisymm _ (le_add_left _ _),
-  rw [omega, ← lift_one.{0}, ← lift_add, lift_le, ← type_unit, type_add],
+  rw [omega, ← lift_one.{0}, ← lift_add, lift_le, ← type_unit, ← type_sum_lex],
   refine ⟨rel_embedding.collapse (rel_embedding.of_monotone _ _)⟩,
   { apply sum.rec, exact λ _, 0, exact nat.succ },
   { intros a b, cases a; cases b; intro H; cases H with _ _ H _ _ H;
@@ -586,12 +586,12 @@ instance : monoid ordinal.{u} :=
     ⟨⟨prod_punit _, λ a b, by rcases a with ⟨a, ⟨⟨⟩⟩⟩; rcases b with ⟨b, ⟨⟨⟩⟩⟩;
     simp only [prod.lex_def, empty_relation, and_false, or_false]; refl⟩⟩ }
 
-@[simp] theorem type_mul {α β : Type u} (r : α → α → Prop) (s : β → β → Prop)
+@[simp] theorem type_prod_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop)
   [is_well_order α r] [is_well_order β s] : type (prod.lex s r) = type r * type s := rfl
 
 private theorem mul_eq_zero' {a b : ordinal} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
 induction_on a $ λ α _ _, induction_on b $ λ β _ _, begin
-  simp_rw [←type_mul, type_eq_zero_iff_is_empty],
+  simp_rw [←type_prod_lex, type_eq_zero_iff_is_empty],
   rw or_comm,
   exact is_empty_prod
 end

src/set_theory/ordinal/basic.lean

@@ -965,8 +965,8 @@ instance : add_monoid_with_one ordinal.{u} :=
 @[simp] theorem card_add (o₁ o₂ : ordinal) : card (o₁ + o₂) = card o₁ + card o₂ :=
 induction_on o₁ $ λ α r _, induction_on o₂ $ λ β s _, rfl
 
-@[simp] theorem type_add {α β : Type u} (r : α → α → Prop) (s : β → β → Prop)
-  [is_well_order α r] [is_well_order β s] : type r + type s = type (sum.lex r s) := rfl
+@[simp] theorem type_sum_lex {α β : Type u} (r : α → α → Prop) (s : β → β → Prop)
+  [is_well_order α r] [is_well_order β s] : type (sum.lex r s) = type r + type s := rfl
 
 @[simp] theorem card_nat (n : ℕ) : card.{u} n = n :=
 by induction n; [refl, simp only [card_add, card_one, nat.cast_succ, *]]