refactor(set_theory/cardinal/*): cardinal.succ → order.succ (#14273)

src/data/W/cardinal.lean

@@ -74,7 +74,7 @@ calc cardinal.sum (λ a : α, m ^ #(β a))
     rw [hn],
     exact power_nat_le (le_max_right _ _)
   end))
-  (pos_iff_ne_zero.1 (succ_le_iff.1
+  (pos_iff_ne_zero.1 (order.succ_le_iff.1
     begin
       rw [succ_zero],
       obtain ⟨a⟩ : nonempty α, from hn,

src/set_theory/cardinal/basic.lean

@@ -30,7 +30,7 @@ We define cardinal numbers as a quotient of types under the equivalence relation
   (contrast with `ℕ : Type`, which lives in a specific universe).
   In some cases the universe level has to be given explicitly.
 * `cardinal.min (I : nonempty ι) (c : ι → cardinal)` is the minimal cardinal in the range of `c`.
-* `cardinal.succ c` is the successor cardinal, the smallest cardinal larger than `c`.
+* `order.succ c` is the successor cardinal, the smallest cardinal larger than `c`.
 * `cardinal.sum` is the sum of a collection of cardinals.
 * `cardinal.sup` is the supremum of a collection of cardinals.
 * `cardinal.powerlt c₁ c₂` or `c₁ ^< c₂` is defined as `sup_{γ < β} α^γ`.
@@ -65,7 +65,7 @@ cardinal number, cardinal arithmetic, cardinal exponentiation, omega,
 Cantor's theorem, König's theorem, Konig's theorem
 -/
 
-open function set
+open function set order
 open_locale classical
 
 noncomputable theory
@@ -529,31 +529,16 @@ cardinal.wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (cardin
 
 instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.wf⟩
 
-/-- The set in the definition of `cardinal.succ` is nonempty. -/
-theorem succ_nonempty (c : cardinal) : {c' : cardinal | c < c'}.nonempty := ⟨_, cantor c⟩
-
-/-- The successor cardinal - the smallest cardinal greater than
-  `c`. This is not the same as `c + 1` except in the case of finite `c`. -/
-def succ (c : cardinal) : cardinal :=
-Inf {c' | c < c'}
-
-theorem lt_succ (c : cardinal) : c < succ c :=
-Inf_mem (succ_nonempty c)
-
-theorem succ_le_iff {a b : cardinal} : succ a ≤ b ↔ a < b :=
-⟨(lt_succ a).trans_le, λ h, cInf_le' h⟩
-
+/-- Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`. -/
 instance : succ_order cardinal :=
-succ_order.of_succ_le_iff succ (λ a b, succ_le_iff)
+succ_order.of_succ_le_iff (λ c, Inf {c' | c < c'})
+  (λ a b, ⟨lt_of_lt_of_le $ Inf_mem $ exists_gt a, cInf_le'⟩)
 
-theorem le_succ : ∀ a, a ≤ succ a := order.le_succ
-theorem lt_succ_iff {a b : cardinal} : a < succ b ↔ a ≤ b := order.lt_succ_iff
-theorem succ_le_of_lt {a b : cardinal} : a < b → succ a ≤ b := order.succ_le_of_lt
-theorem le_of_lt_succ {a b : cardinal} : a < succ b → a ≤ b := order.le_of_lt_succ
+theorem succ_def (c : cardinal) : succ c = Inf {c' | c < c'} := rfl
 
 theorem add_one_le_succ (c : cardinal.{u}) : c + 1 ≤ succ c :=
 begin
-  refine (le_cInf_iff'' (succ_nonempty c)).2 (λ b hlt, _),
+  refine (le_cInf_iff'' (exists_gt c)).2 (λ b hlt, _),
   rcases ⟨b, c⟩ with ⟨⟨β⟩, ⟨γ⟩⟩,
   cases le_of_lt hlt with f,
   have : ¬ surjective f := λ hn, (not_le_of_lt hlt) (mk_le_of_surjective hn),
@@ -563,7 +548,7 @@ begin
           ... ≤ #β          : (f.option_elim b hb).cardinal_le
 end
 
-lemma succ_pos (c : cardinal) : 0 < succ c := order.bot_lt_succ c
+lemma succ_pos : ∀ c : cardinal, 0 < succ c := bot_lt_succ
 
 lemma succ_ne_zero (c : cardinal) : succ c ≠ 0 := (succ_pos _).ne'
 
@@ -887,8 +872,7 @@ nat.cast_injective
 @[simp, norm_cast, priority 900] theorem nat_succ (n : ℕ) : (n.succ : cardinal) = succ n :=
 (add_one_le_succ _).antisymm (succ_le_of_lt $ nat_cast_lt.2 $ nat.lt_succ_self _)
 
-@[simp] theorem succ_zero : succ 0 = 1 :=
-by norm_cast
+@[simp] theorem succ_zero : succ (0 : cardinal) = 1 := by norm_cast
 
 theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : finset α, s.card ≤ n) :
   # α ≤ n :=
@@ -902,7 +886,7 @@ begin
 end
 
 theorem cantor' (a) {b : cardinal} (hb : 1 < b) : a < b ^ a :=
-by rw [← succ_le_iff, (by norm_cast : succ 1 = 2)] at hb;
+by rw [← succ_le_iff, (by norm_cast : succ (1 : cardinal) = 2)] at hb;
    exact (cantor a).trans_le (power_le_power_right hb)
 
 theorem one_le_iff_pos {c : cardinal} : 1 ≤ c ↔ 0 < c :=
@@ -1482,8 +1466,8 @@ end
 lemma three_le {α : Type*} (h : 3 ≤ # α) (x : α) (y : α) :
   ∃ (z : α), z ≠ x ∧ z ≠ y :=
 begin
-  have : ((3:nat) : cardinal) ≤ # α, simpa using h,
-  have : ((2:nat) : cardinal) < # α, rwa [← cardinal.succ_le_iff, ← cardinal.nat_succ],
+  have : ↑(3 : ℕ) ≤ # α, simpa using h,
+  have : ↑(2 : ℕ) < # α, rwa [← succ_le_iff, ← cardinal.nat_succ],
   have := exists_not_mem_of_length_le [x, y] this,
   simpa [not_or_distrib] using this,
 end
@@ -1518,7 +1502,7 @@ end
 lemma powerlt_le_powerlt_left {a b c : cardinal} (h : b ≤ c) : a ^< b ≤ a ^< c :=
 by { rw [powerlt, sup_le_iff], exact λ ⟨s, hs⟩, le_powerlt (lt_of_lt_of_le hs h) }
 
-lemma powerlt_succ {c₁ c₂ : cardinal} (h : c₁ ≠ 0) : c₁ ^< c₂.succ = c₁ ^ c₂ :=
+lemma powerlt_succ {c₁ c₂ : cardinal} (h : c₁ ≠ 0) : c₁ ^< (succ c₂) = c₁ ^ c₂ :=
 begin
   apply le_antisymm,
   { rw powerlt_le, intros c₃ h2, apply power_le_power_left h, rwa [←lt_succ_iff] },

src/set_theory/cardinal/cofinality.lean

@@ -62,13 +62,12 @@ def cof (r : α → α → Prop) [is_refl α r] : cardinal :=
   ⟨⟨set.univ, λ a, ⟨a, ⟨⟩, refl _⟩⟩⟩
   (λ S, #S)
 
-lemma cof_le (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀a, ∃(b ∈ S), r a b) :
-  order.cof r ≤ #S :=
+lemma cof_le (r : α → α → Prop) [is_refl α r] {S : set α} (h : ∀a, ∃(b ∈ S), r a b) : cof r ≤ #S :=
 le_trans (cardinal.min_le _ ⟨S, h⟩) le_rfl
 
 lemma le_cof {r : α → α → Prop} [is_refl α r] (c : cardinal) :
-  c ≤ order.cof r ↔ ∀ {S : set α} (h : ∀a, ∃(b ∈ S), r a b) , c ≤ #S :=
-by { rw [order.cof, cardinal.le_min], exact ⟨λ H S h, H ⟨S, h⟩, λ H ⟨S, h⟩, H h ⟩ }
+  c ≤ cof r ↔ ∀ {S : set α} (h : ∀a, ∃(b ∈ S), r a b) , c ≤ #S :=
+by { rw [cof, cardinal.le_min], exact ⟨λ H S h, H ⟨S, h⟩, λ H ⟨S, h⟩, H h ⟩ }
 
 end order
 
@@ -388,7 +387,7 @@ begin
     { refine λ a, ⟨sum.inr punit.star, set.mem_singleton _, _⟩,
       rcases a with a|⟨⟨⟨⟩⟩⟩; simp [empty_relation] },
     { rw [cardinal.mk_fintype, set.card_singleton], simp } },
-  { rw [← cardinal.succ_zero, cardinal.succ_le_iff],
+  { rw [← cardinal.succ_zero, succ_le_iff],
     simpa [lt_iff_le_and_ne, cardinal.zero_le] using
       λ h, succ_ne_zero o (cof_eq_zero.1 (eq.symm h)) }
 end
@@ -619,7 +618,7 @@ le_antisymm (cof_le_card _) begin
   let g := λ a, (f a).1,
   let o := succ (sup.{u u} g),
   rcases H o with ⟨b, h, l⟩,
-  refine l (order.lt_succ_iff.2 _),
+  refine l (lt_succ_iff.2 _),
   rw ← show g (f.symm ⟨b, h⟩) = b, by dsimp [g]; simp,
   apply le_sup
 end
@@ -739,7 +738,7 @@ theorem is_regular_omega : is_regular ω :=
 theorem is_regular_succ {c : cardinal.{u}} (h : ω ≤ c) : is_regular (succ c) :=
 ⟨h.trans (lt_succ c).le, begin
   refine (cof_ord_le _).antisymm (succ_le_of_lt _),
-  cases quotient.exists_rep (succ c) with α αe, simp at αe,
+  cases quotient.exists_rep (@succ cardinal _ _ c) with α αe, simp at αe,
   rcases ord_eq α with ⟨r, wo, re⟩, resetI,
   have := ord_is_limit (h.trans (lt_succ _).le),
   rw [← αe, re] at this ⊢,
@@ -762,10 +761,10 @@ theorem is_regular_aleph_one : is_regular (aleph 1) :=
 by { rw ← succ_omega, exact is_regular_succ le_rfl }
 
 theorem is_regular_aleph'_succ {o : ordinal} (h : ordinal.omega ≤ o) :
-  is_regular (aleph' (order.succ o)) :=
+  is_regular (aleph' (succ o)) :=
 by { rw aleph'_succ, exact is_regular_succ (omega_le_aleph'.2 h) }
 
-theorem is_regular_aleph_succ (o : ordinal) : is_regular (aleph (order.succ o)) :=
+theorem is_regular_aleph_succ (o : ordinal) : is_regular (aleph (succ o)) :=
 by { rw aleph_succ, exact is_regular_succ (omega_le_aleph o) }
 
 /--
@@ -777,7 +776,7 @@ theorem infinite_pigeonhole_card_lt {β α : Type u} (f : β → α)
   ∃ a : α, #α < #(f ⁻¹' {a}) :=
 begin
   simp_rw [← succ_le_iff],
-  exact ordinal.infinite_pigeonhole_card f (#α).succ (succ_le_of_lt w)
+  exact ordinal.infinite_pigeonhole_card f (succ (#α)) (succ_le_of_lt w)
     (w'.trans (lt_succ _).le)
     ((lt_succ _).trans_le (is_regular_succ w').2.ge),
 end
@@ -906,7 +905,7 @@ begin
   { intros b hb hb',
     rw deriv_family_succ,
     exact nfp_family_lt_ord_lift hω (by rwa hc.2) hf
-      ((ord_is_limit hc.1).2 _ (hb ((order.lt_succ b).trans hb'))) },
+      ((ord_is_limit hc.1).2 _ (hb ((lt_succ b).trans hb'))) },
   { intros b hb H hb',
     rw deriv_family_limit f hb,
     exact bsup_lt_ord_of_is_regular hc (ord_lt_ord.1 ((ord_card_le b).trans_lt hb'))

src/set_theory/cardinal/continuum.lean

@@ -49,7 +49,7 @@ lemma continuum_pos : 0 < 𝔠 := nat_lt_continuum 0
 lemma continuum_ne_zero : 𝔠 ≠ 0 := continuum_pos.ne'
 
 lemma aleph_one_le_continuum : aleph 1 ≤ 𝔠 :=
-by { rw ← succ_omega, exact succ_le_of_lt omega_lt_continuum }
+by { rw ← succ_omega, exact order.succ_le_of_lt omega_lt_continuum }
 
 /-!
 ### Addition

src/set_theory/cardinal/ordinal.lean

@@ -152,16 +152,16 @@ cardinal.aleph_idx.rel_iso.to_equiv.apply_symm_apply o
 by rw [← nonpos_iff_eq_zero, ← aleph'_aleph_idx 0, aleph'_le];
    apply ordinal.zero_le
 
-@[simp] theorem aleph'_succ {o : ordinal.{u}} : aleph' (order.succ o) = (aleph' o).succ :=
+@[simp] theorem aleph'_succ {o : ordinal.{u}} : aleph' (succ o) = succ (aleph' o) :=
 begin
-  apply (succ_le_of_lt $ aleph'_lt.2 $ order.lt_succ o).antisymm' (cardinal.aleph_idx_le.1 $ _),
-  rw [aleph_idx_aleph', order.succ_le_iff, ← aleph'_lt, aleph'_aleph_idx],
-  apply cardinal.lt_succ
+  apply (succ_le_of_lt $ aleph'_lt.2 $ lt_succ o).antisymm' (cardinal.aleph_idx_le.1 $ _),
+  rw [aleph_idx_aleph', succ_le_iff, ← aleph'_lt, aleph'_aleph_idx],
+  apply lt_succ
 end
 
 @[simp] theorem aleph'_nat : ∀ n : ℕ, aleph' n = n
 | 0     := aleph'_zero
-| (n+1) := show aleph' (order.succ n) = n.succ,
+| (n+1) := show aleph' (succ n) = n.succ,
            by rw [aleph'_succ, aleph'_nat, nat_succ]
 
 theorem aleph'_le_of_limit {o : ordinal.{u}} (l : o.is_limit) {c} :
@@ -202,8 +202,8 @@ begin
   { rw [max_eq_left h, max_eq_left (aleph_le.1 h)] }
 end
 
-@[simp] theorem aleph_succ {o : ordinal.{u}} : aleph (order.succ o) = (aleph o).succ :=
-by rw [aleph, ordinal.add_succ, aleph'_succ]; refl
+@[simp] theorem aleph_succ {o : ordinal.{u}} : aleph (succ o) = succ (aleph o) :=
+by { rw [aleph, ordinal.add_succ, aleph'_succ], refl }
 
 @[simp] theorem aleph_zero : aleph 0 = ω :=
 by simp only [aleph, add_zero, aleph'_omega]
@@ -239,7 +239,7 @@ theorem exists_aleph {c : cardinal} : ω ≤ c ↔ ∃ o, c = aleph o :=
  λ ⟨o, e⟩, e.symm ▸ omega_le_aleph _⟩
 
 theorem aleph'_is_normal : is_normal (ord ∘ aleph') :=
-⟨λ o, ord_lt_ord.2 $ aleph'_lt.2 $ order.lt_succ o,
+⟨λ o, ord_lt_ord.2 $ aleph'_lt.2 $ lt_succ o,
  λ o l a, by simp only [ord_le, aleph'_le_of_limit l]⟩
 
 theorem aleph_is_normal : is_normal (ord ∘ aleph) :=
@@ -329,7 +329,7 @@ begin
   rcases typein_surj s h with ⟨p, rfl⟩,
   rw [← e, lt_ord],
   refine lt_of_le_of_lt
-    (_ : _ ≤ card (order.succ (typein (<) (g p))) * card (order.succ (typein (<) (g p)))) _,
+    (_ : _ ≤ card (succ (typein (<) (g p))) * card (succ (typein (<) (g p)))) _,
   { have : {q | s q p} ⊆ insert (g p) {x | x < g p} ×ˢ insert (g p) {x | x < g p},
     { intros q h,
       simp only [s, embedding.coe_fn_mk, order.preimage, typein_lt_typein, prod.lex_def, typein_inj]
@@ -341,7 +341,7 @@ begin
     refine (equiv.set.insert _).trans
       ((equiv.refl _).sum_congr punit_equiv_punit),
     apply @irrefl _ r },
-  cases lt_or_le (card (order.succ (typein (<) (g p)))) ω with qo qo,
+  cases lt_or_le (card (succ (typein (<) (g p)))) ω with qo qo,
   { exact lt_of_lt_of_le (mul_lt_omega qo qo) ol },
   { suffices, {exact lt_of_le_of_lt (IH _ this qo) this},
     rw ← lt_ord, apply (ord_is_limit ol).2,