F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
hx : ∀ (i : ι), i ∈ s → x ≠ v i
⊢ (eval x (nodal s fun i => v i) * ∑ i in s, nodalWeight s (fun i => v i) i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s fun i => v i) * ∑ i in s, nodalWeight s (fun i => v i) i * (x - v i)⁻¹ * OfNat.ofNat 1 i) =
    (∑ i in s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i in s, nodalWeight s v i * (x - v i)⁻¹
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
hx : ∀ (i : ι), i ∈ s → x ≠ v i
⊢ eval x (↑(interpolate s v) r) =
    (∑ i in s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i in s, nodalWeight s v i * (x - v i)⁻¹
rw [← div_one (eval x (interpolate s v r)), ← @eval_one _ _ x, ← interpolate_one hvs hs,
  eval_interpolate_not_at_node r hx, eval_interpolate_not_at_node 1 hx]
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
inst✝ : DecidableEq ι
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
hx : ∀ (i : ι), i ∈ s → x ≠ v i
⊢ (eval x (nodal s fun i => v i) * ∑ i in s, nodalWeight s (fun i => v i) i * (x - v i)⁻¹ * r i) /
      (eval x (nodal s fun i => v i) * ∑ i in s, nodalWeight s (fun i => v i) i * (x - v i)⁻¹ * OfNat.ofNat 1 i) =
    (∑ i in s, nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i in s, nodalWeight s v i * (x - v i)⁻¹
simp only [mul_div_mul_left _ _ (eval_nodal_not_at_node hx), Pi.one_apply, mul_one]