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
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
rcases h with ⟨s, hs⟩
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
⊢ a * ((-b + s) / (2 * a)) * ((-b + s) / (2 * a)) + b * ((-b + s) / (2 * a)) + c = 0
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
use (-b + s) / (2 * a)
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
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
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
⊢ a * ((-b + s) / (2 * a)) * ((-b + s) / (2 * a)) + b * ((-b + s) / (2 * a)) + c = 0
rw [quadratic_eq_zero_iff ha hs]
no goals
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
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
simp