feat(set_theory/ordinal/basic): add gc_ord_card and gci_ord_card (#…

…15152)

Define a Galois coinsertion between `cardinal.ord` and `ordinal.card`,
then use it to golf some proofs.

src/order/galois_connection.lean

@@ -720,7 +720,6 @@ lemma is_lub_of_l_image [preorder α] [preorder β] (gi : galois_coinsertion l u
   (hs : is_lub (l '' s) a) : is_lub s (u a) :=
 gi.dual.is_glb_of_u_image hs
 
-
 section lift
 
 variables [partial_order α]

src/set_theory/ordinal/basic.lean

@@ -902,30 +902,31 @@ let ⟨r, _, e⟩ := ord_eq α in begin
     exact le_trans (ord_le_type _) (type_le'.2 ⟨g⟩) }
 end
 
-theorem lt_ord {c o} : o < ord c ↔ o.card < c :=
-by rw [← not_le, ← not_le, ord_le]
+theorem gc_ord_card : galois_connection ord card := λ _ _, ord_le
+
+theorem lt_ord {c o} : o < ord c ↔ o.card < c := gc_ord_card.lt_iff_lt
 
 @[simp] theorem card_ord (c) : (ord c).card = c :=
 quotient.induction_on c $ λ α,
 let ⟨r, _, e⟩ := ord_eq α in by simp only [mk_def, e, card_type]
 
-theorem ord_card_le (o : ordinal) : o.card.ord ≤ o :=
-ord_le.2 le_rfl
+/-- Galois coinsertion between `cardinal.ord` and `ordinal.card`. -/
+def gci_ord_card : galois_coinsertion ord card :=
+gc_ord_card.to_galois_coinsertion $ λ c, c.card_ord.le
 
-lemma lt_ord_succ_card (o : ordinal) : o < (succ o.card).ord :=
-by { rw lt_ord, apply lt_succ }
+theorem ord_card_le (o : ordinal) : o.card.ord ≤ o := gc_ord_card.l_u_le _
 
-@[simp] theorem ord_le_ord {c₁ c₂} : ord c₁ ≤ ord c₂ ↔ c₁ ≤ c₂ :=
-by simp only [ord_le, card_ord]
+lemma lt_ord_succ_card (o : ordinal) : o < (succ o.card).ord := lt_ord.2 $ lt_succ _
 
-@[simp] theorem ord_lt_ord {c₁ c₂} : ord c₁ < ord c₂ ↔ c₁ < c₂ :=
-by simp only [lt_ord, card_ord]
+@[mono] theorem ord_strict_mono : strict_mono ord := gci_ord_card.strict_mono_l
+@[mono] theorem ord_mono : monotone ord := gc_ord_card.monotone_l
 
-@[simp] theorem ord_zero : ord 0 = 0 :=
-le_antisymm (ord_le.2 $ zero_le _) (ordinal.zero_le _)
+@[simp] theorem ord_le_ord {c₁ c₂} : ord c₁ ≤ ord c₂ ↔ c₁ ≤ c₂ := gci_ord_card.l_le_l_iff
+@[simp] theorem ord_lt_ord {c₁ c₂} : ord c₁ < ord c₂ ↔ c₁ < c₂ := ord_strict_mono.lt_iff_lt
+@[simp] theorem ord_zero : ord 0 = 0 := gc_ord_card.l_bot
 
 @[simp] theorem ord_nat (n : ℕ) : ord n = n :=
-le_antisymm (ord_le.2 $ by simp only [card_nat]) $ begin
+(ord_le.2 (card_nat n).ge).antisymm begin
   induction n with n IH,
   { apply ordinal.zero_le },
   { exact succ_le_of_lt (IH.trans_lt $ ord_lt_ord.2 $ nat_cast_lt.2 (nat.lt_succ_self n)) }
@@ -935,14 +936,11 @@ end
 by simpa using ord_nat 1
 
 @[simp] theorem lift_ord (c) : (ord c).lift = ord (lift c) :=
-eq_of_forall_ge_iff $ λ o, le_iff_le_iff_lt_iff_lt.2 $ begin
-  split; intro h,
-  { rcases ordinal.lt_lift_iff.1 h with ⟨a, e, h⟩,
-    rwa [← e, lt_ord, ← lift_card, lift_lt, ← lt_ord] },
-  { rw lt_ord at h,
-    rcases lift_down' (le_of_lt h) with ⟨o, rfl⟩,
-    rw [← lift_card, lift_lt] at h,
-    rwa [ordinal.lift_lt, lt_ord] }
+begin
+  refine le_antisymm (le_of_forall_lt (λ a ha, _)) _,
+  { rcases ordinal.lt_lift_iff.1 ha with ⟨a, rfl, h⟩,
+    rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← ordinal.lift_lt] },
+  { rw [ord_le, ← lift_card, card_ord] }
 end
 
 lemma mk_ord_out (c : cardinal) : #c.ord.out.α = c := by simp