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
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
refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
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
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
rw [discrim] at h
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
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
have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha
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
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
apply mul_left_cancel₀ ha
no goals
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
linear_combination -h