[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
⊢ x /ᵒᶠ 0 = x
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(x /ᵒᶠ 0) x✝ = ↑x x✝
[PROOFSTEP]
simp only [AddMonoidAlgebra.divOf_apply, zero_add]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a b : G
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a b x✝ : G
⊢ ↑(x /ᵒᶠ (a + b)) x✝ = ↑(x /ᵒᶠ a /ᵒᶠ b) x✝
[PROOFSTEP]
simp only [AddMonoidAlgebra.divOf_apply, add_assoc]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
⊢ of' k G a * x /ᵒᶠ a = x
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(of' k G a * x /ᵒᶠ a) x✝ = ↑x x✝
[PROOFSTEP]
rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ∀ (a_1 : G), a + a_1 = a + x✝ ↔ a_1 = x✝
[PROOFSTEP]
intro c
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
x : AddMonoidAlgebra k G
x✝ c : G
⊢ a + c = a + x✝ ↔ c = x✝
[PROOFSTEP]
exact add_right_inj _
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a : G
⊢ x * of' k G a /ᵒᶠ a = x
[PROOFSTEP]
refine
  Finsupp.ext fun _ =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ : G
⊢ ↑(x * of' k G a /ᵒᶠ a) x✝ = ↑x x✝
[PROOFSTEP]
rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ : G
⊢ ∀ (a_1 : G), a_1 + a = a + x✝ ↔ a_1 = x✝
[PROOFSTEP]
intro c
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ c : G
⊢ c + a = a + x✝ ↔ c = x✝
[PROOFSTEP]
rw [add_comm]
[GOAL]
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
a x✝ c : G
⊢ a + c = a + x✝ ↔ c = x✝
[PROOFSTEP]
exact add_right_inj _
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
a : G
⊢ of' k G a /ᵒᶠ a = 1
[PROOFSTEP]
simpa only [one_mul] using mul_of'_divOf (1 : AddMonoidAlgebra k G) a
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ∃ d, g' = g + d
⊢ ¬¬∃ g₂, g' = g + g₂
[PROOFSTEP]
rwa [Classical.not_not]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
⊢ of' k G g * x %ᵒᶠ g = 0
[PROOFSTEP]
refine
  Finsupp.ext fun g' =>
    ?_
      -- porting note: `ext g'` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
g' : G
⊢ ↑(of' k G g * x %ᵒᶠ g) g' = ↑0 g'
[PROOFSTEP]
rw [Finsupp.zero_apply]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
g' : G
⊢ ↑(of' k G g * x %ᵒᶠ g) g' = 0
[PROOFSTEP]
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
d : G
⊢ ↑(of' k G g * x %ᵒᶠ g) (g + d) = 0
[PROOFSTEP]
rw [modOf_apply_self_add]
[GOAL]
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * x %ᵒᶠ g) g' = 0
[PROOFSTEP]
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x * of' k G g %ᵒᶠ g = 0
[PROOFSTEP]
refine
  Finsupp.ext fun g' =>
    ?_
      -- porting note: `ext g'` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = ↑0 g'
[PROOFSTEP]
rw [Finsupp.zero_apply]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
[PROOFSTEP]
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(x * of' k G g %ᵒᶠ g) (g + d) = 0
[PROOFSTEP]
rw [modOf_apply_self_add]
[GOAL]
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(x * of' k G g %ᵒᶠ g) g' = 0
[PROOFSTEP]
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]
[GOAL]
case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ¬∃ d, g' = d + g
[PROOFSTEP]
simpa only [add_comm] using h
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0
[PROOFSTEP]
simpa only [one_mul] using mul_of'_modOf (1 : AddMonoidAlgebra k G) g
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x
[PROOFSTEP]
refine
  Finsupp.ext fun g' =>
    ?_
      -- porting note: `ext` doesn't work
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g) g' = ↑x g'
[PROOFSTEP]
rw [Finsupp.add_apply]
  -- porting note: changed from `simp_rw` which can't see through the type
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
[PROOFSTEP]
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) + ↑(x %ᵒᶠ g) (g + d) = ↑x (g + d)
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
[PROOFSTEP]
swap
[GOAL]
case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g g' : G
h : ¬∃ d, g' = g + d
⊢ ↑(of' k G g * (x /ᵒᶠ g)) g' + ↑(x %ᵒᶠ g) g' = ↑x g'
[PROOFSTEP]
rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h, zero_add]
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) + ↑(x %ᵒᶠ g) (g + d) = ↑x (g + d)
[PROOFSTEP]
rw [modOf_apply_self_add, add_zero]
[GOAL]
case inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ↑(of' k G g * (x /ᵒᶠ g)) (g + d) = ↑x (g + d)
[PROOFSTEP]
rw [of'_apply, single_mul_apply_aux _ _ _, one_mul, divOf_apply]
[GOAL]
case inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d : G
⊢ ∀ (a : G), g + a = g + d ↔ a = d
[PROOFSTEP]
intro a
[GOAL]
case inl.intro.H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g d a : G
⊢ g + a = g + d ↔ a = d
[PROOFSTEP]
exact add_right_inj _
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x
[PROOFSTEP]
rw [add_comm, divOf_add_modOf]
[GOAL]
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mp.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
⊢ of' k G g * x %ᵒᶠ g = 0
[PROOFSTEP]
rw [of'_mul_modOf]
[GOAL]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x
[PROOFSTEP]
intro h
[GOAL]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x
[PROOFSTEP]
rw [← divOf_add_modOf x g, h, add_zero]
[GOAL]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)
[PROOFSTEP]
exact dvd_mul_right _ _


[GOAL]
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
[GOAL]
case intro.intro
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℕ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
[GOAL]
case intro.intro
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℕ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ f a / gcd s f = g a
[PROOFSTEP]
rw [he a ha, Nat.mul_div_cancel_left]
[GOAL]
case intro.intro.H
β : Type u_1
f : β → ℕ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℕ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ 0 < gcd s f
[PROOFSTEP]
exact Nat.pos_of_ne_zero (mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx)
[GOAL]
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
[GOAL]
case intro.intro
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℤ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
[GOAL]
case intro.intro
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℤ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ f a / gcd s f = g a
[PROOFSTEP]
rw [he a ha, Int.mul_ediv_cancel_left]
[GOAL]
case intro.intro.H
β : Type u_1
f : β → ℤ
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → ℤ
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ gcd s f ≠ 0
[PROOFSTEP]
exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx
[GOAL]
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨x, hx⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → Polynomial K
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
⊢ (gcd s fun b => f b / gcd s f) = 1
[PROOFSTEP]
refine' (Finset.gcd_congr rfl fun a ha => _).trans hg
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → Polynomial K
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ f a / gcd s f = g a
[PROOFSTEP]
rw [he a ha, EuclideanDomain.mul_div_cancel_left]
[GOAL]
case intro.intro.a0
K : Type u_1
inst✝ : Field K
β : Type u_2
f : β → Polynomial K
s : Finset β
x : β
hx : x ∈ s
hfz : f x ≠ 0
g : β → Polynomial K
he : ∀ (b : β), b ∈ s → f b = gcd s f * g b
hg : gcd s g = 1
a : β
ha : a ∈ s
⊢ gcd s f ≠ 0
[PROOFSTEP]
exact mt Finset.gcd_eq_zero_iff.1 fun h => hfz <| h x hx


[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
w x y z : S
⊢ ↑C w * (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    toPoly { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }
[PROOFSTEP]
simp only [toPoly, C_neg, C_add, C_mul]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
w x y z : S
⊢ ↑C w * (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    ↑C w * X ^ 3 + ↑C w * -(↑C x + ↑C y + ↑C z) * X ^ 2 + ↑C w * (↑C x * ↑C y + ↑C x * ↑C z + ↑C y * ↑C z) * X +
      ↑C w * -(↑C x * ↑C y * ↑C z)
[PROOFSTEP]
ring1
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
x y z : S
⊢ (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    toPoly { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }
[PROOFSTEP]
rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
⊢ (∀ (n : ℕ), n > 3 → coeff (toPoly P) n = 0) ∧
    coeff (toPoly P) 3 = P.a ∧ coeff (toPoly P) 2 = P.b ∧ coeff (toPoly P) 1 = P.c ∧ coeff (toPoly P) 0 = P.d
[PROOFSTEP]
simp only [toPoly, coeff_add, coeff_C, coeff_C_mul_X, coeff_C_mul_X_pow]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
⊢ (∀ (n : ℕ),
      n > 3 →
        ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) +
            if n = 0 then P.d else 0) =
          0) ∧
    ((((if True then P.a else 0) + if False then P.b else 0) + if False then P.c else 0) + if False then P.d else 0) =
        P.a ∧
      ((((if False then P.a else 0) + if True then P.b else 0) + if False then P.c else 0) + if False then P.d else 0) =
          P.b ∧
        ((((if False then P.a else 0) + if False then P.b else 0) + if True then P.c else 0) +
              if False then P.d else 0) =
            P.c ∧
          ((((if False then P.a else 0) + if False then P.b else 0) + if False then P.c else 0) +
              if True then P.d else 0) =
            P.d
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
⊢ ∀ (n : ℕ),
    3 < n →
      ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) +
          if n = 0 then P.d else 0) =
        0
[PROOFSTEP]
intro n hn
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) = 0
[PROOFSTEP]
repeat' rw [if_neg]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ (((0 + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ((0 + 0 + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ (0 + 0 + 0 + if n = 0 then P.d else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 1
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 2
[PROOFSTEP]
rw [if_neg]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 3
[PROOFSTEP]
rw [if_neg]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 0
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 1
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 2
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 3
[PROOFSTEP]
any_goals linarith only [hn]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0
[PROOFSTEP]
linarith only [hn]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 0
[PROOFSTEP]
linarith only [hn]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 1
[PROOFSTEP]
linarith only [hn]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 2
[PROOFSTEP]
linarith only [hn]
[GOAL]
case hnc
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 3
[PROOFSTEP]
linarith only [hn]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0
[PROOFSTEP]
repeat' rw [zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 = 0
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 = 0
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h : toPoly P = toPoly Q
⊢ P.a = Q.a
[PROOFSTEP]
rw [← coeff_eq_a, h, coeff_eq_a]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h : toPoly P = toPoly Q
⊢ P.b = Q.b
[PROOFSTEP]
rw [← coeff_eq_b, h, coeff_eq_b]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h : toPoly P = toPoly Q
⊢ P.c = Q.c
[PROOFSTEP]
rw [← coeff_eq_c, h, coeff_eq_c]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h : toPoly P = toPoly Q
⊢ P.d = Q.d
[PROOFSTEP]
rw [← coeff_eq_d, h, coeff_eq_d]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
⊢ toPoly P = ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d
[PROOFSTEP]
rw [toPoly, ha, C_0, zero_mul, zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ toPoly P = ↑C P.c * X + ↑C P.d
[PROOFSTEP]
rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ toPoly P = ↑C P.d
[PROOFSTEP]
rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ toPoly P = 0
[PROOFSTEP]
rw [of_c_eq_zero ha hb hc, hd, C_0]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ toPoly P = 0 ↔ P = 0
[PROOFSTEP]
rw [← zero, toPoly_injective]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0
⊢ toPoly P ≠ 0
[PROOFSTEP]
contrapose! h0
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : toPoly P = 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0
[PROOFSTEP]
rw [(toPoly_eq_zero_iff P).mp h0]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : toPoly P = 0
⊢ 0.a = 0 ∧ 0.b = 0 ∧ 0.c = 0 ∧ 0.d = 0
[PROOFSTEP]
exact ⟨rfl, rfl, rfl, rfl⟩
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ leadingCoeff (toPoly P) = P.b
[PROOFSTEP]
rw [of_a_eq_zero ha, leadingCoeff_quadratic hb]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ leadingCoeff (toPoly P) = P.c
[PROOFSTEP]
rw [of_b_eq_zero ha hb, leadingCoeff_linear hc]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ leadingCoeff (toPoly P) = P.d
[PROOFSTEP]
rw [of_c_eq_zero ha hb hc, leadingCoeff_C]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 1
⊢ Monic (toPoly P)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
[PROOFSTEP]
rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
⊢ Monic (toPoly P)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
[PROOFSTEP]
rw [Monic, leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero), hb]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
⊢ Monic (toPoly P)
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
✝ : Nontrivial R
⊢ Monic (toPoly P)
[PROOFSTEP]
rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 1
⊢ Monic (toPoly P)
[PROOFSTEP]
rw [Monic, leadingCoeff_of_c_eq_zero ha hb hc, hd]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ (fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 })
      ((fun P =>
          { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
        P) =
    P
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 })
        ((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          P)).a =
    P.a
[PROOFSTEP]
simp only [Subtype.coe_mk, coeffs]
[GOAL]
case b
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 })
        ((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          P)).b =
    P.b
[PROOFSTEP]
simp only [Subtype.coe_mk, coeffs]
[GOAL]
case c
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 })
        ((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          P)).c =
    P.c
[PROOFSTEP]
simp only [Subtype.coe_mk, coeffs]
[GOAL]
case d
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 })
        ((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          P)).d =
    P.d
[PROOFSTEP]
simp only [Subtype.coe_mk, coeffs]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ (fun P => { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
      ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) f) =
    f
[PROOFSTEP]
ext (_ | _ | _ | _ | n)
[GOAL]
case a.a.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff
      (↑((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) f)))
      Nat.zero =
    coeff (↑f) Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
[GOAL]
case a.a.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff
      (↑((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) f)))
      (Nat.succ Nat.zero) =
    coeff (↑f) (Nat.succ Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
[GOAL]
case a.a.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff
      (↑((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) f)))
      (Nat.succ (Nat.succ Nat.zero)) =
    coeff (↑f) (Nat.succ (Nat.succ Nat.zero))
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
[GOAL]
case a.a.succ.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff
      (↑((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) f)))
      (Nat.succ (Nat.succ (Nat.succ Nat.zero))) =
    coeff (↑f) (Nat.succ (Nat.succ (Nat.succ Nat.zero)))
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
[GOAL]
case a.a.succ.succ.succ.succ
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
⊢ coeff
      (↑((fun P =>
            { val := toPoly P, property := (_ : degree (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) ≤ 3) })
          ((fun f => { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) f)))
      (Nat.succ (Nat.succ (Nat.succ (Nat.succ n)))) =
    coeff (↑f) (Nat.succ (Nat.succ (Nat.succ (Nat.succ n))))
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.succ_eq_add_one]
[GOAL]
case a.a.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 0 = coeff (↑f) 0
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (0 + 1) =
    coeff (↑f) (0 + 1)
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (1 + 1) =
    coeff (↑f) (1 + 1)
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.succ.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (1 + 1 + 1) =
    coeff (↑f) (1 + 1 + 1)
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.succ.succ.succ.succ
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (n + 3 + 1) =
    coeff (↑f) (n + 3 + 1)
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 0 = coeff (↑f) 0
[PROOFSTEP]
try simp only [coeffs]
[GOAL]
case a.a.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 0 = coeff (↑f) 0
[PROOFSTEP]
simp only [coeffs]
[GOAL]
case a.a.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 1 = coeff (↑f) 1
[PROOFSTEP]
try simp only [coeffs]
[GOAL]
case a.a.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 1 = coeff (↑f) 1
[PROOFSTEP]
simp only [coeffs]
[GOAL]
case a.a.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 2 = coeff (↑f) 2
[PROOFSTEP]
try simp only [coeffs]
[GOAL]
case a.a.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 2 = coeff (↑f) 2
[PROOFSTEP]
simp only [coeffs]
[GOAL]
case a.a.succ.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 3 = coeff (↑f) 3
[PROOFSTEP]
try simp only [coeffs]
[GOAL]
case a.a.succ.succ.succ.zero
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) 3 = coeff (↑f) 3
[PROOFSTEP]
simp only [coeffs]
[GOAL]
case a.a.succ.succ.succ.succ
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (4 + n) =
    coeff (↑f) (4 + n)
[PROOFSTEP]
try simp only [coeffs]
[GOAL]
case a.a.succ.succ.succ.succ
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (4 + n) =
    coeff (↑f) (4 + n)
[PROOFSTEP]
simp only [coeffs]
[GOAL]
case a.a.succ.succ.succ.succ
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (4 + n) =
    coeff (↑f) (4 + n)
[PROOFSTEP]
have h3 : 3 < 4 + n := by linarith only
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
⊢ 3 < 4 + n
[PROOFSTEP]
linarith only
[GOAL]
case a.a.succ.succ.succ.succ
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
h3 : 3 < 4 + n
⊢ coeff (toPoly { a := coeff (↑f) 3, b := coeff (↑f) 2, c := coeff (↑f) 1, d := coeff (↑f) 0 }) (4 + n) =
    coeff (↑f) (4 + n)
[PROOFSTEP]
rw [coeff_eq_zero h3, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2 _ <| WithBot.coe_lt_coe.mpr (by exact h3)]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // degree p ≤ 3 }
n : ℕ
h3 : 3 < 4 + n
⊢ ↑3 < ↑(4 + n)
[PROOFSTEP]
exact h3
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
⊢ degree (toPoly P) ≤ 2
[PROOFSTEP]
simpa only [of_a_eq_zero ha] using degree_quadratic_le
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ degree (toPoly P) = 2
[PROOFSTEP]
rw [of_a_eq_zero ha, degree_quadratic hb]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ degree (toPoly P) ≤ 1
[PROOFSTEP]
simpa only [of_b_eq_zero ha hb] using degree_linear_le
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ degree (toPoly P) = 1
[PROOFSTEP]
rw [of_b_eq_zero ha hb, degree_linear hc]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ degree (toPoly P) ≤ 0
[PROOFSTEP]
simpa only [of_c_eq_zero ha hb hc] using degree_C_le
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d ≠ 0
⊢ degree (toPoly P) = 0
[PROOFSTEP]
rw [of_c_eq_zero ha hb hc, degree_C hd]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ degree (toPoly P) = ⊥
[PROOFSTEP]
rw [of_d_eq_zero ha hb hc hd, degree_zero]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
⊢ natDegree (toPoly P) ≤ 2
[PROOFSTEP]
simpa only [of_a_eq_zero ha] using natDegree_quadratic_le
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ natDegree (toPoly P) = 2
[PROOFSTEP]
rw [of_a_eq_zero ha, natDegree_quadratic hb]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ natDegree (toPoly P) ≤ 1
[PROOFSTEP]
simpa only [of_b_eq_zero ha hb] using natDegree_linear_le
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ natDegree (toPoly P) = 1
[PROOFSTEP]
rw [of_b_eq_zero ha hb, natDegree_linear hc]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ natDegree (toPoly P) = 0
[PROOFSTEP]
rw [of_c_eq_zero ha hb hc, natDegree_C]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : Semiring S
φ : R →+* S
⊢ toPoly (map φ P) = Polynomial.map φ (toPoly P)
[PROOFSTEP]
simp only [map, toPoly, map_C, map_X, Polynomial.map_add, Polynomial.map_mul, Polynomial.map_pow]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain S
⊢ roots (map φ P) = Polynomial.roots (Polynomial.map φ (toPoly P))
[PROOFSTEP]
rw [roots, map_toPoly]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain R
h0 : toPoly P ≠ 0
x : R
⊢ x ∈ roots P ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
[PROOFSTEP]
rw [roots, mem_roots h0, IsRoot, toPoly]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝² : CommRing R
inst✝¹ : CommRing S
φ : R →+* S
inst✝ : IsDomain R
h0 : toPoly P ≠ 0
x : R
⊢ eval x (↑C P.a * X ^ 3 + ↑C P.b * X ^ 2 + ↑C P.c * X + ↑C P.d) = 0 ↔ P.a * x ^ 3 + P.b * x ^ 2 + P.c * x + P.d = 0
[PROOFSTEP]
simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ Finset.card (toFinset (roots P)) ≤ 3
[PROOFSTEP]
apply (toFinset_card_le P.toPoly.roots).trans
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
[PROOFSTEP]
by_cases hP : P.toPoly = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
[PROOFSTEP]
exact (card_roots' P.toPoly).trans (by rw [hP, natDegree_zero]; exact zero_le 3)
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ natDegree (toPoly P) ≤ 3
[PROOFSTEP]
rw [hP, natDegree_zero]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ 0 ≤ 3
[PROOFSTEP]
exact zero_le 3
[GOAL]
case neg
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬toPoly P = 0
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
[PROOFSTEP]
exact WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
⊢ Splits φ (toPoly P) ↔ ↑card (roots (map φ P)) = 3
[PROOFSTEP]
replace ha : (map φ P).a ≠ 0 := (_root_.map_ne_zero φ).mpr ha
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : (map φ P).a ≠ 0
⊢ Splits φ (toPoly P) ↔ ↑card (roots (map φ P)) = 3
[PROOFSTEP]
nth_rw 1 [← RingHom.id_comp φ]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : (map φ P).a ≠ 0
⊢ Splits (RingHom.comp (RingHom.id K) φ) (toPoly P) ↔ ↑card (roots (map φ P)) = 3
[PROOFSTEP]
rw [roots, ← splits_map_iff, ← map_toPoly, Polynomial.splits_iff_card_roots, ←
  ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
⊢ Splits φ (toPoly P) ↔ ∃ x y z, roots (map φ P) = {x, y, z}
[PROOFSTEP]
rw [splits_iff_card_roots ha, card_eq_three]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ toPoly (map φ P) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
[PROOFSTEP]
rw [map_toPoly,
  eq_prod_roots_of_splits <|
    (splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
  leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑C (↑φ P.a) * prod (Multiset.map (fun a => X - ↑C a) {x, y, z}) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
[PROOFSTEP]
change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑C (↑φ P.a) * prod ((X - ↑C x) ::ₘ (X - ↑C y) ::ₘ {X - ↑C z}) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
[PROOFSTEP]
rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ map φ P =
    { a := ↑φ P.a, b := ↑φ P.a * -(x + y + z), c := ↑φ P.a * (x * y + x * z + y * z), d := ↑φ P.a * -(x * y * z) }
[PROOFSTEP]
apply_fun @toPoly _ _
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ toPoly (map φ P) =
    toPoly
      { a := ↑φ P.a, b := ↑φ P.a * -(x + y + z), c := ↑φ P.a * (x * y + x * z + y * z), d := ↑φ P.a * -(x * y * z) }
[PROOFSTEP]
rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]
[GOAL]
case inj
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ Function.Injective toPoly
[PROOFSTEP]
exact fun P Q ↦ (toPoly_injective P Q).mp
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ P.b = ↑φ P.a * -(x + y + z)
[PROOFSTEP]
injection eq_sum_three_roots ha h3
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ P.c = ↑φ P.a * (x * y + x * z + y * z)
[PROOFSTEP]
injection eq_sum_three_roots ha h3
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ P.d = ↑φ P.a * -(x * y * z)
[PROOFSTEP]
injection eq_sum_three_roots ha h3
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ (disc P) = (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
[PROOFSTEP]
simp only [disc, RingHom.map_add, RingHom.map_sub, RingHom.map_mul, map_pow]
  -- Porting note: Replaced `simp only [RingHom.map_one, map_bit0, map_bit1]` with f4, f18, f27
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
[PROOFSTEP]
have f4 : φ 4 = 4 := map_natCast φ 4
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
f4 : ↑φ 4 = 4
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
[PROOFSTEP]
have f18 : φ 18 = 18 := map_natCast φ 18
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
[PROOFSTEP]
have f27 : φ 27 = 27 := map_natCast φ 27
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
f27 : ↑φ 27 = 27
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
[PROOFSTEP]
rw [f4, f18, f27, b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
f27 : ↑φ 27 = 27
⊢ (↑φ P.a * -(x + y + z)) ^ 2 * (↑φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * ↑φ P.a * (↑φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (↑φ P.a * -(x + y + z)) ^ 3 * (↑φ P.a * -(x * y * z)) -
        27 * ↑φ P.a ^ 2 * (↑φ P.a * -(x * y * z)) ^ 2 +
      18 * ↑φ P.a * (↑φ P.a * -(x + y + z)) * (↑φ P.a * (x * y + x * z + y * z)) * (↑φ P.a * -(x * y * z)) =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
[PROOFSTEP]
ring1
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ disc P ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
[PROOFSTEP]
rw [← _root_.map_ne_zero φ, disc_eq_prod_three_roots ha h3, pow_two]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z) * (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
[PROOFSTEP]
simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha, and_assoc]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ disc P ≠ 0 ↔ Nodup (roots (map φ P))
[PROOFSTEP]
rw [disc_ne_zero_iff_roots_ne ha h3, h3]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup {x, y, z}
[PROOFSTEP]
change _ ↔ (x ::ₘ y ::ₘ { z }).Nodup
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup (x ::ₘ y ::ₘ {z})
[PROOFSTEP]
rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup {z}
[PROOFSTEP]
simp only [nodup_singleton]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
[PROOFSTEP]
tauto
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
hd : disc P ≠ 0
⊢ Finset.card (toFinset (roots (map φ P))) = 3
[PROOFSTEP]
rw [toFinset_card_of_nodup <| (disc_ne_zero_iff_roots_nodup ha h3).mp hd, ← splits_iff_card_roots ha,
  splits_iff_roots_eq_three ha]
[GOAL]
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
hd : disc P ≠ 0
⊢ ∃ x y z, roots (map φ P) = {x, y, z}
[PROOFSTEP]
exact ⟨x, ⟨y, ⟨z, h3⟩⟩⟩