chore(order/bounded_lattice): make bot_lt_some and some_lt_none c…

…onsistent (#9180)

`with_bot.bot_lt_some` gets renamed to `with_bot.none_lt_some` and now syntactically applies to `none : with_bot α` (`with_bot.bot_le_coe` already applies to `⊥` and `↑a`).
`with_top.some_lt_none` now takes `a` explicit.

src/data/nat/with_bot.lean

@@ -42,7 +42,7 @@ lemma with_bot.one_le_iff_zero_lt {x : with_bot ℕ} : 1 ≤ x ↔ 0 < x :=
 begin
   refine ⟨λ h, lt_of_lt_of_le (with_bot.coe_lt_coe.mpr zero_lt_one) h, λ h, _⟩,
   induction x using with_bot.rec_bot_coe,
-  { exact false.elim (not_lt_of_lt (with_bot.bot_lt_some 0) h) },
+  { exact (not_lt_bot h).elim },
   { exact with_bot.coe_le_coe.mpr (nat.succ_le_iff.mpr (with_bot.coe_lt_coe.mp h)) }
 end
 

src/data/polynomial/degree/definitions.lean

@@ -853,7 +853,7 @@ begin
       ≤ finset.univ.fold (⊔) ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) : degree_sum_le _ _
   ... = finset.univ.fold max ⊥ (λ i, (C (f i) * X ^ (i : ℕ)).degree) :
     (@finset.fold_hom _ _ _ (⊔) _ _ _ ⊥ finset.univ _ _ _ id (with_bot.sup_eq_max)).symm
-  ... < n : (finset.fold_max_lt (n : with_bot ℕ)).mpr ⟨with_bot.bot_lt_some _, _⟩,
+  ... < n : (finset.fold_max_lt (n : with_bot ℕ)).mpr ⟨with_bot.bot_lt_coe _, _⟩,
 
   rintros ⟨i, hi⟩ -,
   calc (C (f ⟨i, hi⟩) * X ^ i).degree

src/data/polynomial/div.lean

@@ -253,7 +253,7 @@ have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne hp0,
 if hpq : degree p < degree q
 then begin
   rw [(div_by_monic_eq_zero_iff hq hq0).2 hpq, degree_eq_nat_degree hp0],
-  exact with_bot.bot_lt_some _
+  exact with_bot.bot_lt_coe _
 end
 else begin
   rw [← degree_add_div_by_monic hq (not_lt.1 hpq), degree_eq_nat_degree hq0,

src/order/bounded_lattice.lean

@@ -512,10 +512,11 @@ instance has_lt [has_lt α] : has_lt (with_bot α) :=
   @has_lt.lt (with_bot α) _ (some a) (some b) ↔ a < b :=
 by simp [(<)]
 
-lemma bot_lt_some [has_lt α] (a : α) : (⊥ : with_bot α) < some a :=
+lemma none_lt_some [has_lt α] (a : α) :
+  @has_lt.lt (with_bot α) _ none (some a) :=
 ⟨a, rfl, λ b hb, (option.not_mem_none _ hb).elim⟩
 
-lemma bot_lt_coe [has_lt α] (a : α) : (⊥ : with_bot α) < a := bot_lt_some a
+lemma bot_lt_coe [has_lt α] (a : α) : (⊥ : with_bot α) < a := none_lt_some a
 
 instance : can_lift (with_bot α) α :=
 { coe := coe,
@@ -761,7 +762,7 @@ by simp [(≤)]
   @has_le.le (with_top α) _ a none :=
 by simp [(≤)]
 
-@[simp] theorem some_lt_none [has_lt α] {a : α} :
+@[simp] theorem some_lt_none [has_lt α] (a : α) :
   @has_lt.lt (with_top α) _ (some a) none :=
 by simp [(<)]; existsi a; refl
 
@@ -821,7 +822,7 @@ theorem lt_iff_exists_coe [partial_order α] : ∀{a b : with_top α}, a < b ↔
 @[norm_cast]
 lemma coe_lt_coe [partial_order α] {a b : α} : (a : with_top α) < b ↔ a < b := some_lt_some
 
-lemma coe_lt_top [partial_order α] (a : α) : (a : with_top α) < ⊤ := some_lt_none
+lemma coe_lt_top [partial_order α] (a : α) : (a : with_top α) < ⊤ := some_lt_none a
 
 theorem coe_lt_iff [partial_order α] {a : α} : ∀{x : with_top α}, ↑a < x ↔ (∀b:α, x = ↑b → a < b)
 | (some b) := by simp [some_eq_coe, coe_eq_coe, coe_lt_coe]

src/ring_theory/power_basis.lean

@@ -100,7 +100,7 @@ begin
     refine ⟨f, _, hy⟩,
     by_cases hf : f = 0,
     { simp only [hf, nat_degree_zero, degree_zero] at h ⊢,
-      exact lt_of_le_of_ne (nat.zero_le d) hd.symm <|> exact with_bot.bot_lt_some d },
+      exact lt_of_le_of_ne (nat.zero_le d) hd.symm <|> exact with_bot.bot_lt_coe d },
     simpa only [degree_eq_nat_degree hf, with_bot.coe_lt_coe] using h },
 end