case refine'_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
⊢ ↑derivative (nodal ∅ v) = ∑ i in ∅, nodal (Finset.erase ∅ i) v

case refine'_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : Finset ι
hit : ¬x✝¹ ∈ x✝
IH : ↑derivative (nodal x✝ v) = ∑ i in x✝, nodal (Finset.erase x✝ i) v
⊢ ↑derivative (nodal (insert x✝¹ x✝) v) = ∑ i in insert x✝¹ x✝, nodal (Finset.erase (insert x✝¹ x✝) i) v
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
⊢ ↑derivative (nodal s v) = ∑ i in s, nodal (Finset.erase s i) v
refine' Finset.induction_on s _ fun _ _ hit IH => _
no goals
case refine'_1
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
⊢ ↑derivative (nodal ∅ v) = ∑ i in ∅, nodal (Finset.erase ∅ i) v
rw [nodal_empty, derivative_one, sum_empty]
case refine'_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : Finset ι
hit : ¬x✝¹ ∈ x✝
IH : ↑derivative (nodal x✝ v) = ∑ i in x✝, nodal (Finset.erase x✝ i) v
⊢ ∑ x in x✝, (X - ↑C (v x✝¹)) * nodal (Finset.erase x✝ x) v = ∑ x in x✝, nodal (Finset.erase (insert x✝¹ x✝) x) v
case refine'_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : Finset ι
hit : ¬x✝¹ ∈ x✝
IH : ↑derivative (nodal x✝ v) = ∑ i in x✝, nodal (Finset.erase x✝ i) v
⊢ ↑derivative (nodal (insert x✝¹ x✝) v) = ∑ i in insert x✝¹ x✝, nodal (Finset.erase (insert x✝¹ x✝) i) v
rw [nodal_insert_eq_nodal hit, derivative_mul, IH, derivative_sub, derivative_X, derivative_C,
  sub_zero, one_mul, sum_insert hit, mul_sum, erase_insert hit, add_right_inj]
case refine'_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : Finset ι
hit : ¬x✝¹ ∈ x✝
IH : ↑derivative (nodal x✝ v) = ∑ i in x✝, nodal (Finset.erase x✝ i) v
j : ι
hjt : j ∈ x✝
⊢ (X - ↑C (v x✝¹)) * nodal (Finset.erase x✝ j) v = nodal (Finset.erase (insert x✝¹ x✝) j) v
case refine'_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : Finset ι
hit : ¬x✝¹ ∈ x✝
IH : ↑derivative (nodal x✝ v) = ∑ i in x✝, nodal (Finset.erase x✝ i) v
⊢ ∑ x in x✝, (X - ↑C (v x✝¹)) * nodal (Finset.erase x✝ x) v = ∑ x in x✝, nodal (Finset.erase (insert x✝¹ x✝) x) v
refine' sum_congr rfl fun j hjt => _
no goals
case refine'_2
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
x✝¹ : ι
x✝ : Finset ι
hit : ¬x✝¹ ∈ x✝
IH : ↑derivative (nodal x✝ v) = ∑ i in x✝, nodal (Finset.erase x✝ i) v
j : ι
hjt : j ∈ x✝
⊢ (X - ↑C (v x✝¹)) * nodal (Finset.erase x✝ j) v = nodal (Finset.erase (insert x✝¹ x✝) j) v
rw [nodal_erase_eq_nodal_div (mem_insert_of_mem hjt), nodal_insert_eq_nodal hit,
  EuclideanDomain.mul_div_assoc _ (X_sub_C_dvd_nodal v hjt), nodal_erase_eq_nodal_div hjt]