awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
simp_rw :
  ∏ j ∈ s.erase i, basisDivisor (v i) (v j) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₁ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₂ :
  ∏ x ∈ s.erase i,
      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (v i - v x)⁻¹ : F[X])
        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₃ :
  HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹)
      (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    (C : (a : F) → F[X]) (∏ j ∈ s.erase i, (v i - v j)⁻¹) *
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
simp_rw₄ :
  HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹)
      (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
    (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹) *
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
⊢ Lagrange.basis s v i =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))
have simp_rw₅ : HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹)
    (∏ x ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v x) : F[X])) =
  HMul.hMul (α := F[X]) (∏ x ∈ s.erase i, (C : (a : F) → F[X]) (v i - v x)⁻¹) (nodal (s.erase i) v)
Tactic: simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
    nodal_erase_eq_nodal_div hi, nodal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₁ : eval x
    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
  nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₂ : eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
    eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
  nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₃ : nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
  nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₇ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v i))
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
rw₇ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v i))
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₈ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
  nodalWeight s v i * ((x - v i)⁻¹ * ((x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1)))
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
rw₇ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v i))
rw₈ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * ((x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1)))
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₉ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
  nodalWeight s v i * ((x - v i)⁻¹ * (x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1))
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
rw₇ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v i))
rw₈ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * ((x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1)))
rw₉ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * (x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1))
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₁₀ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
  nodalWeight s v i * HMul.hMul (α := F) 1 (∏ x_1 ∈ s.erase i, (x - v x_1))
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
x : F
hi : i ∈ s
hxi : x ≠ v i
rw : eval x (Lagrange.basis s v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₁ :
  eval x
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v i) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X]))) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₂ :
  eval x ((C : (a : F) → F[X]) (nodalWeight s v i)) *
      eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₃ :
  nodalWeight s v i * eval x (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v i) : F[X])) =
    nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₄ : nodalWeight s v i * eval x (nodal (s.erase i) v) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₅ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * eval x (nodal s v)
rw₆ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * (x - v i)⁻¹ * ∏ i ∈ s, (x - v i)
rw₇ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ((x - v i)⁻¹ * ∏ i ∈ s, (x - v i))
rw₈ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * ((x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1)))
rw₉ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * ((x - v i)⁻¹ * (x - v i) * ∏ x_1 ∈ s.erase i, (x - v x_1))
rw₁₀ :
  nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) =
    nodalWeight s v i * HMul.hMul (α := F) 1 (∏ x_1 ∈ s.erase i, (x - v x_1))
⊢ eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹)
have rw₁₁ : nodalWeight s v i * ∏ i ∈ s.erase i, (x - v i) = nodalWeight s v i * ∏ x_1 ∈ s.erase i, (x - v x_1)
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hi, eval_mul, eval_C, ←
    nodal_erase_eq_nodal_div hi, eval_nodal, eval_nodal, mul_assoc, ← mul_prod_erase _ _ hi, ←
    mul_assoc (x - v i)⁻¹, inv_mul_cancel₀ (sub_ne_zero_of_ne hxi), one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
j : ι
hj : j ∈ s
⊢ HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r j) : F[X]) (Lagrange.basis s v j) =
    HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X])
have rw : HMul.hMul (α := F[X]) (β := F[X]) (Lagrange.basis s v j) ((C : (a : F) → F[X]) (r j) : F[X]) =
  HMul.hMul (β := F[X])
    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
    ((C : (a : F) → F[X]) (r j) : F[X])
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
j : ι
hj : j ∈ s
rw :
  HMul.hMul (α := F[X]) (β := F[X]) (Lagrange.basis s v j) ((C : (a : F) → F[X]) (r j) : F[X]) =
    HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X])
⊢ HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (r j) : F[X]) (Lagrange.basis s v j) =
    HMul.hMul (β := F[X])
      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
        (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
      ((C : (a : F) → F[X]) (r j) : F[X])
have rw₁ : HMul.hMul (β := F[X])
    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
    ((C : (a : F) → F[X]) (r j) : F[X]) =
  HMul.hMul (β := F[X])
    (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (nodalWeight s v j) : F[X])
      (nodal s v / HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (v j) : F[X])))
    ((C : (a : F) → F[X]) (r j) : F[X])
Tactic: rw [mul_comm, basis_eq_prod_sub_inv_mul_nodal_div hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x ((interpolate s v : (a : ι → F) → F[X]) r) =
    eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ * r i
have simp_rw : Eq.{u_1 + 1} (α := F) (∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1))
  (∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i))
Tactic: simp_rw [interpolate_apply, mul_sum, eval_finsetSum, eval_mul, eval_C]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Lagrange (goal)
Goal:
F : Type u_1
inst : Field F
ι : Type u_2
inst_1 : DecidableEq ι
s : Finset ι
v r : ι → F
x : F
hx : ∀ i ∈ s, x ≠ v i
⊢ Eq.{u_1 + 1} (α := F) (∑ x_1 ∈ s, r x_1 * eval x (Lagrange.basis s v x_1))
    (∑ i ∈ s, eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i))
have refine : ∀ (i : ι) (hi : i ∈ s),
  r i * eval x (Lagrange.basis s v i) = eval x (nodal s v) * (nodalWeight s v i * (x - v i)⁻¹ * r i)
Tactic: refine sum_congr rfl fun i hi => ?_