feat(set_theory/{ordinal, ordinal_arithmetic}): Add various instances…

… for `o.out.α` (#12508)

src/measure_theory/card_measurable_space.lean

@@ -93,7 +93,6 @@ theorem generate_measurable_subset_rec (s : set (set α)) ⦃t : set α⦄
   (ht : generate_measurable s t) :
   t ∈ ⋃ i, generate_measurable_rec s i :=
 begin
-  haveI : nonempty ω₁, by simp [← mk_ne_zero_iff, ne_of_gt, (aleph 1).mk_ord_out, aleph_pos 1],
   inhabit ω₁,
   induction ht with u hu u hu IH f hf IH,
   { refine mem_Union.2 ⟨default, _⟩,
@@ -103,8 +102,8 @@ begin
     rw generate_measurable_rec,
     simp only [union_singleton, mem_union_eq, mem_insert_iff, eq_self_iff_true, true_or] },
   { rcases mem_Union.1 IH with ⟨i, hi⟩,
-    obtain ⟨j, hj⟩ : ∃ j, i < j := ordinal.has_succ_of_is_limit
-      (by { rw ordinal.type_lt, exact ord_aleph_is_limit 1 }) _,
+    obtain ⟨j, hj⟩ : ∃ j, i < j := ordinal.has_succ_of_type_succ_lt
+      (by { rw ordinal.type_lt, exact (ord_aleph_is_limit 1).2 }) _,
     apply mem_Union.2 ⟨j, _⟩,
     rw generate_measurable_rec,
     have : ∃ a, (a < j) ∧ u ∈ generate_measurable_rec s a := ⟨i, hj, hi⟩,

src/set_theory/cardinal_ordinal.lean

@@ -213,6 +213,12 @@ by rwa [←aleph'_zero, aleph'_lt]
 theorem aleph_pos (o : ordinal) : 0 < aleph o :=
 omega_pos.trans_le (omega_le_aleph o)
 
+instance (o : ordinal) : nonempty (aleph o).ord.out.α :=
+begin
+  rw [out_nonempty_iff_ne_zero, ←ord_zero],
+  exact λ h, (ord_injective h).not_gt (aleph_pos o)
+end
+
 theorem ord_aleph_is_limit (o : ordinal) : is_limit (aleph o).ord :=
 ord_is_limit $ omega_le_aleph _
 

src/set_theory/ordinal.lean

@@ -790,12 +790,12 @@ begin
   exact not_lt_of_le (ordinal.zero_le _) this
 end
 
-instance : is_empty (0 : ordinal.{u}).out.α :=
-by rw out_empty_iff_eq_zero
-
 @[simp] theorem out_nonempty_iff_ne_zero {o : ordinal} : nonempty o.out.α ↔ o ≠ 0 :=
 by rw [←not_iff_not, ←not_is_empty_iff, not_not, not_not, out_empty_iff_eq_zero]
 
+instance : is_empty (0 : ordinal).out.α :=
+out_empty_iff_eq_zero.2 rfl
+
 instance : has_one ordinal :=
 ⟨⟦⟨punit, empty_relation, by apply_instance⟩⟧⟩
 
@@ -1078,14 +1078,42 @@ instance : is_well_order ordinal (<) := ⟨wf⟩
 
 instance : succ_order ordinal := succ_order.of_succ_le_iff succ (λ _ _, succ_le)
 
+theorem lt_succ {a b : ordinal} : a < succ b ↔ a ≤ b :=
+by rw [← not_le, succ_le, not_lt]
+
 @[simp] lemma typein_le_typein (r : α → α → Prop) [is_well_order α r] {x x' : α} :
   typein r x ≤ typein r x' ↔ ¬r x' x :=
 by rw [←not_lt, typein_lt_typein]
 
+@[simp] lemma typein_le_typein' (o : ordinal) {x x' : o.out.α} :
+  typein (<) x ≤ typein (<) x' ↔ x ≤ x' :=
+by { rw typein_le_typein, exact not_lt }
+
 lemma enum_le_enum (r : α → α → Prop) [is_well_order α r] {o o' : ordinal}
   (ho : o < type r) (ho' : o' < type r) : ¬r (enum r o' ho') (enum r o ho) ↔ o ≤ o' :=
 by rw [←@not_lt _ _ o' o, enum_lt_enum ho']
 
+lemma enum_le_enum' (a : ordinal) {o o' : ordinal} (ho : o < a) (ho' : o' < a) :
+  @enum a.out.α (<) _ o (by rwa type_lt) ≤ @enum a.out.α (<) _ o' (by rwa type_lt) ↔ o ≤ o' :=
+by rw [←enum_le_enum (<), ←not_lt]
+
+theorem enum_zero_le {r : α → α → Prop} [is_well_order α r] (h0 : 0 < type r) (a : α) :
+  ¬ r a (enum r 0 h0) :=
+by { rw [←enum_typein r a, enum_le_enum r], apply ordinal.zero_le }
+
+theorem enum_zero_le' {o : ordinal} (h0 : 0 < o) (a : o.out.α) :
+  @enum o.out.α (<) _ 0 (by rwa type_lt) ≤ a :=
+by { rw ←not_lt, apply enum_zero_le }
+
+theorem le_enum_succ {o : ordinal} (a : o.succ.out.α) :
+  a ≤ @enum o.succ.out.α (<) _ o (by { rw type_lt, exact lt_succ_self o }) :=
+begin
+  rw ←enum_typein (<) a,
+  apply (enum_le_enum' o.succ _ _).2,
+  rw ←lt_succ,
+  all_goals { apply typein_lt_self }
+end
+
 theorem enum_inj {r : α → α → Prop} [is_well_order α r] {o₁ o₂ : ordinal} (h₁ : o₁ < type r)
   (h₂ : o₂ < type r) : enum r o₁ h₁ = enum r o₂ h₂ ↔ o₁ = o₂ :=
 ⟨λ h, begin
@@ -1096,6 +1124,14 @@ theorem enum_inj {r : α → α → Prop} [is_well_order α r] {o₁ o₂ : ordi
     { change _ < _ at hlt, rwa [←@enum_lt_enum α r _ o₂ o₁ h₂ h₁, h] at hlt }
 end, λ h, by simp_rw h⟩
 
+/-- `o.out.α` is an `order_bot` whenever `0 < o`. -/
+def out_order_bot_of_pos {o : ordinal} (ho : 0 < o) : order_bot o.out.α :=
+⟨_, enum_zero_le' ho⟩
+
+theorem enum_zero_eq_bot {o : ordinal} (ho : 0 < o) :
+  enum (<) 0 (by rwa type_lt) = by { haveI H := out_order_bot_of_pos ho, exact ⊥ } :=
+rfl
+
 /-- `univ.{u v}` is the order type of the ordinals of `Type u` as a member
   of `ordinal.{v}` (when `u < v`). It is an inaccessible cardinal. -/
 @[nolint check_univs] -- intended to be used with explicit universe parameters

src/set_theory/ordinal_arithmetic.lean

@@ -123,9 +123,6 @@ theorem nat_cast_succ (n : ℕ) : (succ n : ordinal) = n.succ := 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]
 
-theorem lt_succ {a b : ordinal} : a < succ b ↔ a ≤ b :=
-by rw [← not_le, succ_le, not_lt]
-
 theorem lt_one_iff_zero {a : ordinal} : a < 1 ↔ a = 0 :=
 by rw [←succ_zero, lt_succ, ordinal.le_zero]
 
@@ -182,6 +179,9 @@ type_ne_zero_iff_nonempty.2 ⟨punit.star⟩
 instance : nontrivial ordinal.{u} :=
 ⟨⟨1, 0, ordinal.one_ne_zero⟩⟩
 
+instance : nonempty (1 : ordinal).out.α :=
+out_nonempty_iff_ne_zero.2 ordinal.one_ne_zero
+
 theorem zero_lt_one : (0 : ordinal) < 1 :=
 lt_iff_le_and_ne.2 ⟨ordinal.zero_le _, ne.symm $ ordinal.one_ne_zero⟩
 
@@ -341,13 +341,23 @@ end
 by rw [limit_rec_on, well_founded.fix_eq,
        dif_neg h.1, dif_neg (not_succ_of_is_limit h)]; refl
 
-lemma has_succ_of_is_limit {α} {r : α → α → Prop} [wo : is_well_order α r]
-  (h : (type r).is_limit) (x : α) : ∃y, r x y :=
+instance (o : ordinal) : order_top o.succ.out.α :=
+⟨_, le_enum_succ⟩
+
+theorem enum_succ_eq_top {o : ordinal} :
+  enum (<) o (by { rw type_lt, apply lt_succ_self }) = (⊤ : o.succ.out.α) :=
+rfl
+
+lemma has_succ_of_type_succ_lt {α} {r : α → α → Prop} [wo : is_well_order α r]
+  (h : ∀ a < type r, succ a < type r) (x : α) : ∃ y, r x y :=
 begin
-  use enum r (typein r x).succ (h.2 _ (typein_lt_type r x)),
+  use enum r (typein r x).succ (h _ (typein_lt_type r x)),
   convert (enum_lt_enum (typein_lt_type r x) _).mpr (lt_succ_self _), rw [enum_typein]
 end
 
+theorem out_no_max_of_succ_lt {o : ordinal} (ho : ∀ a < o, succ a < o) : no_max_order o.out.α :=
+⟨has_succ_of_type_succ_lt (by rwa type_lt)⟩
+
 lemma type_subrel_lt (o : ordinal.{u}) :
   type (subrel (<) {o' : ordinal | o' < o}) = ordinal.lift.{u+1} o :=
 begin