refactor(order/conditionally_complete_lattice): tweak `well_founded.c…

…onditionally_complete_linear_order_with_bot` (#14706)

We change the `well_founded` assumption on `well_founded.conditionally_complete_linear_order_bot` to an equivalent but more convenient `is_well_order` typeclass assumption. As such, we place it in the `is_well_order` namespace.

src/order/conditionally_complete_lattice.lean

@@ -132,35 +132,32 @@ instance complete_linear_order.to_conditionally_complete_linear_order_bot {α :
 section
 open_locale classical
 
-/-- A well founded linear order with a bottom element is conditionally complete. -/
-@[reducible] noncomputable def well_founded.conditionally_complete_linear_order_with_bot
-  {α : Type*} [i₁ : linear_order α] [i₂ : order_bot α] (h : well_founded ((<) : α → α → Prop)) :
+/-- A well founded linear order is conditionally complete, with a bottom element. -/
+@[reducible] noncomputable def is_well_order.conditionally_complete_linear_order_bot
+  (α : Type*) [i₁ : linear_order α] [i₂ : order_bot α] [h : is_well_order α (<)] :
   conditionally_complete_linear_order_bot α :=
-{ Inf := λ s, if hs : s.nonempty then h.min s hs else ⊥,
+{ Inf := λ s, if hs : s.nonempty then h.wf.min s hs else ⊥,
   cInf_le := λ s a hs has, begin
     have s_ne : s.nonempty := ⟨a, has⟩,
-    simpa [s_ne] using not_lt.1 (h.not_lt_min s s_ne has),
+    simpa [s_ne] using not_lt.1 (h.wf.not_lt_min s s_ne has),
   end,
   le_cInf := λ s a hs has, begin
     simp only [hs, dif_pos],
-    exact has (h.min_mem s hs),
+    exact has (h.wf.min_mem s hs),
   end,
-  Sup := λ s, if hs : (upper_bounds s).nonempty then h.min _ hs else ⊥,
+  Sup := λ s, if hs : (upper_bounds s).nonempty then h.wf.min _ hs else ⊥,
   le_cSup := λ s a hs has, begin
     have h's : (upper_bounds s).nonempty := hs,
     simp only [h's, dif_pos],
-    exact h.min_mem _ h's has,
+    exact h.wf.min_mem _ h's has,
   end,
   cSup_le := λ s a hs has, begin
     have h's : (upper_bounds s).nonempty := ⟨a, has⟩,
     simp only [h's, dif_pos],
-    simpa using h.not_lt_min _ h's has,
+    simpa using h.wf.not_lt_min _ h's has,
   end,
-  cSup_empty := begin
-    simp only [univ_nonempty, dif_pos, upper_bounds_empty],
-    exact bot_unique (h.min_le $ mem_univ ⊥)
-  end,
-  .. i₁, .. i₂, .. linear_order.to_lattice }
+  cSup_empty := by simpa using eq_bot_iff.2 (not_lt.1 $ h.wf.not_lt_min _ _ $ mem_univ ⊥),
+  ..i₁, ..i₂, ..linear_order.to_lattice }
 
 end
 

src/order/well_founded.lean

@@ -46,7 +46,11 @@ theorem has_min {α} {r : α → α → Prop} (H : well_founded r)
 | ⟨a, ha⟩ := (acc.rec_on (H.apply a) $ λ x _ IH, not_imp_not.1 $ λ hne hx, hne $
   ⟨x, hx, λ y hy hyx, hne $ IH y hyx hy⟩) ha
 
-/-- A minimal element of a nonempty set in a well-founded order -/
+/-- A minimal element of a nonempty set in a well-founded order.
+
+If you're working with a nonempty linear order, consider defining a
+`conditionally_complete_linear_order_bot` instance via
+`well_founded.conditionally_complete_linear_order_with_bot` and using `Inf` instead. -/
 noncomputable def min {r : α → α → Prop} (H : well_founded r)
   (p : set α) (h : p.nonempty) : α :=
 classical.some (H.has_min p h)

src/set_theory/cardinal/basic.lean

@@ -521,11 +521,11 @@ end⟩
 
 instance : has_well_founded cardinal.{u} := ⟨(<), cardinal.lt_wf⟩
 
-instance : conditionally_complete_linear_order_bot cardinal :=
-cardinal.lt_wf.conditionally_complete_linear_order_with_bot
-
 instance wo : @is_well_order cardinal.{u} (<) := ⟨cardinal.lt_wf⟩
 
+instance : conditionally_complete_linear_order_bot cardinal :=
+is_well_order.conditionally_complete_linear_order_bot _
+
 @[simp] theorem Inf_empty : Inf (∅ : set cardinal.{u}) = 0 :=
 dif_neg not_nonempty_empty
 

src/set_theory/ordinal/basic.lean

@@ -763,6 +763,9 @@ type_ne_zero_iff_nonempty.2 h
 protected theorem zero_le (o : ordinal) : 0 ≤ o :=
 induction_on o $ λ α r _, ⟨⟨⟨embedding.of_is_empty, is_empty_elim⟩, is_empty_elim⟩⟩
 
+instance : order_bot ordinal :=
+⟨0, ordinal.zero_le⟩
+
 @[simp] protected theorem le_zero {o : ordinal} : o ≤ 0 ↔ o = 0 :=
 by simp only [le_antisymm_iff, ordinal.zero_le, and_true]
 
@@ -1196,10 +1199,8 @@ let ⟨i, e⟩ := min_eq I (lift ∘ f) in
 by rw e; exact lift_le.2 (le_min.2 $ λ j, lift_le.1 $
 by have := min_le (lift ∘ f) j; rwa e at this)
 
-instance : order_bot ordinal := ⟨0, ordinal.zero_le⟩
-
 instance : conditionally_complete_linear_order_bot ordinal :=
-lt_wf.conditionally_complete_linear_order_with_bot
+is_well_order.conditionally_complete_linear_order_bot _
 
 @[simp] lemma bot_eq_zero : (⊥ : ordinal) = 0 := rfl