refactor(data/polynomial/degree): use with_bot.unbot' instead of `o…

…ption.get_or_else` (#17120)

src/data/polynomial/degree/definitions.lean

@@ -42,7 +42,7 @@ inv_image.wf degree (with_bot.well_founded_lt nat.lt_wf)
 instance : has_well_founded R[X] := ⟨_, degree_lt_wf⟩
 
 /-- `nat_degree p` forces `degree p` to ℕ, by defining nat_degree 0 = 0. -/
-def nat_degree (p : R[X]) : ℕ := (degree p).get_or_else 0
+def nat_degree (p : R[X]) : ℕ := (degree p).unbot' 0
 
 /-- `leading_coeff p` gives the coefficient of the highest power of `X` in `p`-/
 def leading_coeff (p : R[X]) : R := coeff p (nat_degree p)
@@ -106,7 +106,7 @@ option.some_inj.1 $ show (nat_degree p : with_bot ℕ) = n,
   by rwa [← degree_eq_nat_degree hp0]
 
 @[simp] lemma degree_le_nat_degree : degree p ≤ nat_degree p :=
-with_bot.gi_get_or_else_bot.gc.le_u_l _
+with_bot.gi_unbot'_bot.gc.le_u_l _
 
 lemma nat_degree_eq_of_degree_eq [semiring S] {q : S[X]} (h : degree p = degree q) :
   nat_degree p = nat_degree q :=
@@ -153,20 +153,20 @@ end
 
 lemma degree_ne_of_nat_degree_ne {n : ℕ} :
   p.nat_degree ≠ n → degree p ≠ n :=
-mt $ λ h, by rw [nat_degree, h, option.get_or_else_coe]
+mt $ λ h, by rw [nat_degree, h, with_bot.unbot'_coe]
 
 theorem nat_degree_le_iff_degree_le {n : ℕ} : nat_degree p ≤ n ↔ degree p ≤ n :=
-with_bot.get_or_else_bot_le_iff
+with_bot.unbot'_bot_le_iff
 
 lemma nat_degree_lt_iff_degree_lt (hp : p ≠ 0) :
   p.nat_degree < n ↔ p.degree < ↑n :=
-with_bot.get_or_else_bot_lt_iff $ degree_eq_bot.not.mpr hp
+with_bot.unbot'_lt_iff $ degree_eq_bot.not.mpr hp
 
 alias nat_degree_le_iff_degree_le ↔ ..
 
 lemma nat_degree_le_nat_degree [semiring S] {q : S[X]} (hpq : p.degree ≤ q.degree) :
   p.nat_degree ≤ q.nat_degree :=
-with_bot.gi_get_or_else_bot.gc.monotone_l hpq
+with_bot.gi_unbot'_bot.gc.monotone_l hpq
 
 @[simp] lemma degree_C (ha : a ≠ 0) : degree (C a) = (0 : with_bot ℕ) :=
 by rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,

src/order/bounded_order.lean

@@ -693,25 +693,19 @@ lemma map_le_iff [preorder α] [preorder β] (f : α → β) (mono_iff : ∀ {a
 | (a : α) ⊥       := by simp only [map_coe, map_bot, coe_ne_bot, not_coe_le_bot _]
 | (a : α) (b : α) := by simpa using mono_iff
 
-lemma le_coe_get_or_else [preorder α] : ∀ (a : with_bot α) (b : α), a ≤ a.get_or_else b
-| (some a) b := le_refl a
-| none     b := λ _ h, option.no_confusion h
+lemma le_coe_unbot' [preorder α] : ∀ (a : with_bot α) (b : α), a ≤ a.unbot' b
+| (a : α) b := le_rfl
+| ⊥       b := bot_le
 
-@[simp] lemma get_or_else_bot (a : α) : option.get_or_else (⊥ : with_bot α) a = a := rfl
-
-lemma get_or_else_bot_le_iff [has_le α] [order_bot α] {a : with_bot α} {b : α} :
-  a.get_or_else ⊥ ≤ b ↔ a ≤ b :=
+lemma unbot'_bot_le_iff [has_le α] [order_bot α] {a : with_bot α} {b : α} :
+  a.unbot' ⊥ ≤ b ↔ a ≤ b :=
 by cases a; simp [none_eq_bot, some_eq_coe]
 
-lemma get_or_else_bot_lt_iff [partial_order α] [order_bot α] {a : with_bot α} {b : α}
-  (ha : a ≠ ⊥) :
-  a.get_or_else ⊥ < b ↔ a < b :=
+lemma unbot'_lt_iff [has_lt α] {a : with_bot α} {b c : α} (ha : a ≠ ⊥) :
+  a.unbot' b < c ↔ a < c :=
 begin
-  obtain ⟨a, rfl⟩ := ne_bot_iff_exists.mp ha,
-  simp only [lt_iff_le_and_ne, get_or_else_bot_le_iff, and.congr_right_iff],
-  intro h,
-  apply iff.not,
-  simp only [with_bot.coe_eq_coe, option.get_or_else_coe, iff_self],
+  lift a to α using ha,
+  rw [unbot'_coe, coe_lt_coe]
 end
 
 instance [semilattice_sup α] : semilattice_sup (with_bot α) :=

src/order/galois_connection.lean

@@ -766,11 +766,11 @@ end lift
 
 end galois_coinsertion
 
-/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then
-`λ o : with_bot α, o.get_or_else ⊥` and coercion form a Galois insertion. -/
-def with_bot.gi_get_or_else_bot [preorder α] [order_bot α] :
-  galois_insertion (λ o : with_bot α, o.get_or_else ⊥) coe :=
-{ gc := λ a b, with_bot.get_or_else_bot_le_iff,
+/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then `with_bot.unbot' ⊥` and
+coercion form a Galois insertion. -/
+def with_bot.gi_unbot'_bot [preorder α] [order_bot α] :
+  galois_insertion (with_bot.unbot' ⊥) (coe : α → with_bot α) :=
+{ gc := λ a b, with_bot.unbot'_bot_le_iff,
   le_l_u := λ a, le_rfl,
-  choice := λ o ho, _,
+  choice := λ o ho, o.unbot' ⊥,
   choice_eq := λ _ _, rfl }