chore(algebra/quadratic_discriminant): golf proofs using limits (#5339)

src/algebra/ordered_ring.lean

@@ -393,22 +393,6 @@ lt_of_not_ge (λ ha, absurd h (mul_nonpos_of_nonneg_of_nonpos ha hb).not_lt)
 lemma neg_of_mul_pos_right (h : 0 < a * b) (ha : a ≤ 0) : b < 0 :=
 lt_of_not_ge (λ hb, absurd h (mul_nonpos_of_nonpos_of_nonneg ha hb).not_lt)
 
-lemma exists_lt_mul_self (a : α) : ∃ x : α, a < x * x :=
-begin
-  by_cases ha : 0 ≤ a,
-  { use (a + 1),
-    calc a = a * 1 : by rw mul_one
-    ... < (a + 1) * (a + 1) : mul_lt_mul (lt_add_one _) (le_add_of_nonneg_left ha)
-                                         zero_lt_one (add_nonneg ha zero_le_one) },
-  { rw not_le at ha,
-    use 1,
-    calc a < 0     : ha
-       ... < 1 * 1 : by simpa only [mul_one] using zero_lt_one' }
-end
-
-lemma exists_le_mul_self (a : α) : ∃ x : α, a ≤ x * x :=
-let ⟨x, hx⟩ := exists_lt_mul_self a in ⟨x, le_of_lt hx⟩
-
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_semiring α] :
   no_top_order α :=

src/algebra/quadratic_discriminant.lean

@@ -5,6 +5,7 @@ Authors: Zhouhang Zhou
 -/
 import algebra.invertible
 import tactic.linarith
+import order.filter.at_top_bot
 
 /-!
 # Quadratic discriminants and roots of a quadratic
@@ -28,6 +29,8 @@ This file defines the discriminant of a quadratic and gives the solution to a qu
 polynomial, quadratic, discriminant, root
 -/
 
+open filter
+
 section ring
 variables {R : Type*}
 
@@ -117,27 +120,14 @@ begin
   rw [discrim, pow_two],
   obtain ha|rfl|ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0,
   -- if a < 0
-  { by_cases hb : b = 0,
-    { rw hb at *,
-      rcases exists_lt_mul_self (-c / a) with ⟨x, hx⟩,
-      have := mul_lt_mul_of_neg_left hx ha,
-      rw [mul_div_cancel' _ (ne_of_lt ha), ← mul_assoc] at this,
-      have h₂ := h x, linarith },
-    { by_cases hc' : c = 0,
-      { rw hc' at *,
-        have : -(a * -b * -b + b * -b + 0) = (1 - a) * (b * b), {ring},
-        have h := h (-b), rw [← neg_nonpos, this] at h,
-        have : b * b ≤ 0 := nonpos_of_mul_nonpos_left h (by linarith),
-        linarith },
-      { have h := h (-c / b),
-        have : a * (-c / b) * (-c / b) + b * (-c / b) + c = a * ((c / b) * (c / b)),
-        { rw mul_div_cancel' _ hb, ring },
-        rw this at h,
-        have : 0 ≤ a := nonneg_of_mul_nonneg_right h (mul_self_pos $ div_ne_zero hc' hb),
-        linarith [ha] } } },
+  { have : tendsto (λ x, (a * x + b) * x + c) at_top at_bot :=
+     tendsto_at_bot_add_const_right _ c ((tendsto_at_bot_add_const_right _ b
+       (tendsto_id.neg_const_mul_at_top ha)).at_bot_mul_at_top tendsto_id),
+    rcases (this.eventually (eventually_lt_at_bot 0)).exists with ⟨x, hx⟩,
+    exact false.elim ((h x).not_lt $ by rwa ← add_mul) },
   -- if a = 0
-  { by_cases hb : b = 0,
-    { rw [hb], linarith },
+  { rcases em (b = 0) with (rfl|hb),
+    { simp },
     { have := h ((-c - 1) / b), rw [mul_div_cancel' _ hb] at this, linarith } },
   -- if a > 0
   { have := calc

src/order/filter/at_top_bot.lean

@@ -1121,6 +1121,20 @@ end filter
 
 open filter finset
 
+section
+
+variables {R : Type*} [linear_ordered_semiring R]
+
+lemma exists_lt_mul_self (a : R) : ∃ x ≥ 0, a < x * x :=
+let ⟨x, hxa, hx0⟩ :=((tendsto_mul_self_at_top.eventually (eventually_gt_at_top a)).and
+  (eventually_ge_at_top 0)).exists
+in ⟨x, hx0, hxa⟩
+
+lemma exists_le_mul_self (a : R) : ∃ x ≥ 0, a ≤ x * x :=
+let ⟨x, hx0, hxa⟩ := exists_lt_mul_self a in ⟨x, hx0, hxa.le⟩
+
+end
+
 namespace order_iso
 
 variables [preorder α] [preorder β]