-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials {n : ℕ}
    (v : Fin n → R) (p : Fin n → R[X]) (h_deg : ∀ i, (p i).natDegree ≤ i) :
    Matrix.of (fun i j => ((p j).eval (v i))) =
    (Matrix.vandermonde v) * (Matrix.of (fun (i j : Fin n) => (p j).coeff i))

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ((p j).sum fun e a => (RingHom.id R) a * v i ^ e) =
    ∑ x : Fin n, of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Tactic:
rw [sum_eq_of_subset _ (fun j => zero_mul ((v i) ^ j)) this, ← Fin.sum_univ_eq_sum_range]

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ∑ i_1 : Fin n, (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1 =
    ∑ x : Fin n, of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ∑ i_1 : Fin n, (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1 =
    ∑ x : Fin n, of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Tactic:
congr

Result:
case a.e_f
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ (fun i_1 => (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1) = fun x =>
    of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ of (fun i j => eval (v i) (p j)) i j = (vandermonde v * of fun i j => (p j).coeff ↑i) i j

Tactic:
rw [Matrix.mul_apply, eval, Matrix.of_apply, eval₂]

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a => (RingHom.id R) a * v i ^ e) =
    ∑ j_1 : Fin n, vandermonde v i j_1 * of (fun i j => (p j).coeff ↑i) j_1 j

Proof state:
case a.e_f.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
⊢ (RingHom.id R) ((p j).coeff ↑k) * v i ^ ↑k = of (fun i j => v i ^ ↑j) i k * of (fun i j => (p j).coeff ↑i) k j

Tactic:
rw [mul_comm, Matrix.of_apply, RingHom.id_apply, of_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
⊢ (of fun i j => eval (v i) (p j)) = vandermonde v * of fun i j => (p j).coeff ↑i

Tactic:
ext i j

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ of (fun i j => eval (v i) (p j)) i j = (vandermonde v * of fun i j => (p j).coeff ↑i) i j

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a => (RingHom.id R) a * v i ^ e) =
    ∑ x : Fin n, of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Tactic:
have : (p j).support ⊆ range n := supp_subset_range <| Nat.lt_of_le_of_lt (h_deg j) <| Fin.prop j

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ ((p j).sum fun e a => (RingHom.id R) a * v i ^ e) =
    ∑ x : Fin n, of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a => (RingHom.id R) a * v i ^ e) =
    ∑ j_1 : Fin n, vandermonde v i j_1 * of (fun i j => (p j).coeff ↑i) j_1 j

Tactic:
simp only [eq_intCast, Int.cast_id, Matrix.vandermonde]

Result:
case a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
⊢ ((p j).sum fun e a => (RingHom.id R) a * v i ^ e) =
    ∑ x : Fin n, of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Proof state:
case a.e_f
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
⊢ (fun i_1 => (RingHom.id R) ((p j).coeff ↑i_1) * v i ^ ↑i_1) = fun x =>
    of (fun i j => v i ^ ↑j) i x * of (fun i j => (p j).coeff ↑i) x j

Tactic:
ext k

Result:
case a.e_f.h
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i
i j : Fin n
this : (p j).support ⊆ range n
k : Fin n
⊢ (RingHom.id R) ((p j).coeff ↑k) * v i ^ ↑k = of (fun i j => v i ^ ↑j) i k * of (fun i j => (p j).coeff ↑i) k j