K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ b * b - 4 * a * c ≤ 0
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ discrim a b c ≤ 0
rw [discrim, sq]
case inl
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0

case inr.inl
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0

case inr.inr
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ b * b - 4 * a * c ≤ 0
obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
case inl
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
⊢ b * b - 4 * a * c ≤ 0
case inl
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0
have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
  tendsto_atBot_add_const_right _ c
    ((tendsto_atBot_add_const_right _ b (tendsto_id.neg_const_mul_atTop ha)).atBot_mul_atTop
      tendsto_id)
case inl.intro
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ b * b - 4 * a * c ≤ 0
case inl
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
⊢ b * b - 4 * a * c ≤ 0
rcases(this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
no goals
case inl.intro
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ b * b - 4 * a * c ≤ 0
exact False.elim ((h x).not_lt <| by rwa [← add_mul])
no goals
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : a < 0
this : Tendsto (fun x => (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * x * x + b * x + c < 0
rwa [← add_mul]
case inr.inl.inl
K : Type u_1
inst✝ : LinearOrderedField K
c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0

case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0
case inr.inl
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
⊢ b * b - 4 * 0 * c ≤ 0
rcases eq_or_ne b 0 with (rfl | hb)
no goals
case inr.inl.inl
K : Type u_1
inst✝ : LinearOrderedField K
c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + 0 * x + c
⊢ 0 * 0 - 4 * 0 * c ≤ 0
simp
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b) * ((-c - 1) / b) + b * ((-c - 1) / b) + c
⊢ b * b - 4 * 0 * c ≤ 0
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
⊢ b * b - 4 * 0 * c ≤ 0
have := h ((-c - 1) / b)
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b) * ((-c - 1) / b) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b) * ((-c - 1) / b) + b * ((-c - 1) / b) + c
⊢ b * b - 4 * 0 * c ≤ 0
rw [mul_div_cancel' _ hb] at this
no goals
case inr.inl.inr
K : Type u_1
inst✝ : LinearOrderedField K
b c : K
h : ∀ (x : K), 0 ≤ 0 * x * x + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b) * ((-c - 1) / b) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0
linarith
case inr.inr
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c ≤ 0
case inr.inr
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0
have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
case h.e'_3
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c))
case inr.inr
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c ≤ 0
convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1
case h.e'_3
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ (b * b - 4 * a * c) * (2 * a * (2 * a) * (2 * a)) =
    -(4 * a * (a * b * b * (2 * a) + -(b * b * (2 * a * (2 * a))) + c * (2 * a * (2 * a) * (2 * a))))
case h.e'_3
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c))
field_simp [ha.ne']
no goals
case h.e'_3
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), 0 ≤ a * x * x + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ (b * b - 4 * a * c) * (2 * a * (2 * a) * (2 * a)) =
    -(4 * a * (a * b * b * (2 * a) + -(b * b * (2 * a * (2 * a))) + c * (2 * a * (2 * a) * (2 * a))))
ring