[GOAL]
R : Type u_1
inst✝ : Ring R
a b c : R
⊢ discrim (-a) (-b) (-c) = discrim a b c
[PROOFSTEP]
simp [discrim]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * x * x + b * x + c = 0
⊢ discrim a b c = (2 * a * x + b) ^ 2
[PROOFSTEP]
rw [discrim]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * x * x + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
[PROOFSTEP]
linear_combination -4 * a * h
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
⊢ a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2
[PROOFSTEP]
refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = (2 * a * x + b) ^ 2
⊢ a * x * x + b * x + c = 0
[PROOFSTEP]
rw [discrim] at h 
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
⊢ a * x * x + b * x + c = 0
[PROOFSTEP]
have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ a * x * x + b * x + c = 0
[PROOFSTEP]
apply mul_left_cancel₀ ha
[GOAL]
R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ 2 * 2 * a * (a * x * x + b * x + c) = 2 * 2 * a * 0
[PROOFSTEP]
linear_combination -h
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
[PROOFSTEP]
rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
[PROOFSTEP]
field_simp
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b + s ∨ x * (2 * a) = -b - s
[PROOFSTEP]
apply or_congr
[GOAL]
case h₁
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ↔ x * (2 * a) = -b + s
[PROOFSTEP]
constructor
[GOAL]
case h₁.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b → x * (2 * a) = -b + s
[PROOFSTEP]
intro h'
[GOAL]
case h₁.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ x * (2 * a) = -b + s → s = 2 * a * x + b
[PROOFSTEP]
intro h'
[GOAL]
case h₁.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : s = 2 * a * x + b
⊢ x * (2 * a) = -b + s
[PROOFSTEP]
linear_combination -h'
[GOAL]
case h₁.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : x * (2 * a) = -b + s
⊢ s = 2 * a * x + b
[PROOFSTEP]
linear_combination -h'
[GOAL]
case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = -b + -(2 * a * x) ↔ x * (2 * a) = -b - s
[PROOFSTEP]
constructor
[GOAL]
case h₂.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = -b + -(2 * a * x) → x * (2 * a) = -b - s
[PROOFSTEP]
intro h'
[GOAL]
case h₂.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ x * (2 * a) = -b - s → s = -b + -(2 * a * x)
[PROOFSTEP]
intro h'
[GOAL]
case h₂.mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : s = -b + -(2 * a * x)
⊢ x * (2 * a) = -b - s
[PROOFSTEP]
linear_combination h'
[GOAL]
case h₂.mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
h' : x * (2 * a) = -b - s
⊢ s = -b + -(2 * a * x)
[PROOFSTEP]
linear_combination h'
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
h : ∃ s, discrim a b c = s * s
⊢ ∃ x, a * x * x + b * x + c = 0
[PROOFSTEP]
rcases h with ⟨s, hs⟩
[GOAL]
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ ∃ x, a * x * x + b * x + c = 0
[PROOFSTEP]
use(-b + s) / (2 * a)
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ a * ((-b + s) / (2 * a)) * ((-b + s) / (2 * a)) + b * ((-b + s) / (2 * a)) + c = 0
[PROOFSTEP]
rw [quadratic_eq_zero_iff ha hs]
[GOAL]
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
[PROOFSTEP]
have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ discrim a b c = 0 * 0
[PROOFSTEP]
rw [h, mul_zero]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c x✝ : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = 0 * 0
⊢ a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
[PROOFSTEP]
rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
[GOAL]
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
[PROOFSTEP]
rw [discrim, sq]
[GOAL]
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
[PROOFSTEP]
obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a :=
  lt_trichotomy a
    0
      -- if a < 0
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
rcases(this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
[GOAL]
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
[PROOFSTEP]
exact
  False.elim
    ((h x).not_lt <| by rwa [← add_mul])
      -- if a = 0
[GOAL]
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
[PROOFSTEP]
rwa [← add_mul]
[GOAL]
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
[PROOFSTEP]
rcases eq_or_ne b 0 with (rfl | hb)
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
have := h ((-c - 1) / b)
[GOAL]
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
[PROOFSTEP]
rw [mul_div_cancel' _ hb] at this 
[GOAL]
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
[PROOFSTEP]
linarith
  -- if a > 0
[GOAL]
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
[PROOFSTEP]
have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
[GOAL]
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
[PROOFSTEP]
convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1
[GOAL]
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))
[PROOFSTEP]
field_simp [ha.ne']
[GOAL]
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))))
[PROOFSTEP]
ring
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
h : ∀ (x : K), a * x * x + b * x + c ≤ 0
⊢ ∀ (x : K), 0 ≤ -a * x * x + -b * x + -c
[PROOFSTEP]
simpa only [neg_mul, ← neg_add, neg_nonneg]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
⊢ discrim a b c < 0
[PROOFSTEP]
have : ∀ x : K, 0 ≤ a * x * x + b * x + c := fun x => le_of_lt (h x)
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this : ∀ (x : K), 0 ≤ a * x * x + b * x + c
⊢ discrim a b c < 0
[PROOFSTEP]
refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
⊢ False
[PROOFSTEP]
have := h (-b / (2 * a))
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c
⊢ False
[PROOFSTEP]
have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
  rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
[PROOFSTEP]
rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * x * x + b * x + c
this✝¹ : ∀ (x : K), 0 ≤ a * x * x + b * x + c
h' : discrim a b c = 0
this✝ : 0 < a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c
this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), a * x * x + b * x + c < 0
⊢ ∀ (x : K), 0 < -a * x * x + -b * x + -c
[PROOFSTEP]
simpa only [neg_mul, ← neg_add, neg_pos]
