R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
unfold vandermonde
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
v : Fin Nat.zero → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin Nat.zero, ∏ j in Ioi i, (v j - v i)

case succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n), ∏ j in Ioi i, (v j - v i)
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
induction' n with n ih
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ∀ (i j : Fin (Nat.succ n)),
    ↑of (fun i j => v i ^ ↑j) i j =
      ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) i j +
        vecCons 0 1 i * ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) 0 j

case succ.calc_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
case succ
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n), ∏ j in Ioi i, (v j - v i)
calc
  det (of fun i j : Fin n.succ => v i ^ (j : ℕ)) =
      det
        (of fun i j : Fin n.succ =>
          Matrix.vecCons (v 0 ^ (j : ℕ)) (fun i => v (Fin.succ i) ^ (j : ℕ) - v 0 ^ (j : ℕ)) i) :=
    det_eq_of_forall_row_eq_smul_add_const (Matrix.vecCons 0 1) 0 (Fin.cons_zero _ _) ?_
  _ =
      det
        (of fun i j : Fin n =>
          Matrix.vecCons (v 0 ^ (j.succ : ℕ))
            (fun i : Fin n => v (Fin.succ i) ^ (j.succ : ℕ) - v 0 ^ (j.succ : ℕ))
            (Fin.succAbove 0 i)) := by
    simp_rw [det_succ_column_zero, Fin.sum_univ_succ, of_apply, Matrix.cons_val_zero, submatrix,
      of_apply, Matrix.cons_val_succ, Fin.val_zero, pow_zero, one_mul, sub_self,
      MulZeroClass.mul_zero, MulZeroClass.zero_mul, Finset.sum_const_zero, add_zero]
  _ =
      det
        (of fun i j : Fin n =>
            (v (Fin.succ i) - v 0) *
              ∑ k in Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) :
          Matrix _ _ R) := by
    congr
    ext (i j)
    rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm]
    exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm
  _ =
      (Finset.prod Finset.univ (fun i => v (Fin.succ i) - v 0)) *
        det fun i j : Fin n =>
          ∑ k in Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) :=
    (det_mul_column (fun i => v (Fin.succ i) - v 0) _)
  _ = (Finset.prod Finset.univ (fun i => v (Fin.succ i) - v 0)) *
  det fun i j : Fin n => v (Fin.succ i) ^ (j : ℕ) := congr_arg _ ?_
  _ = ∏ i : Fin n.succ, Finset.prod (Ioi i) (fun j => v j - v i) := by
    simp_rw [Fin.prod_univ_succ, Fin.prod_Ioi_zero, Fin.prod_Ioi_succ]
    have h := ih (v ∘ Fin.succ)
    unfold Function.comp at h
    rw [h]
no goals
case zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
v : Fin Nat.zero → R
⊢ (det fun i j => v i ^ ↑j) = ∏ i : Fin Nat.zero, ∏ j in Ioi i, (v j - v i)
exact det_eq_one_of_card_eq_zero (Fintype.card_fin 0)
no goals
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ det (↑of fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) =
    det
      (↑of fun i j =>
        vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
          (↑(Fin.succAbove 0) i))
simp_rw [det_succ_column_zero, Fin.sum_univ_succ, of_apply, Matrix.cons_val_zero, submatrix,
  of_apply, Matrix.cons_val_succ, Fin.val_zero, pow_zero, one_mul, sub_self,
  MulZeroClass.mul_zero, MulZeroClass.zero_mul, Finset.sum_const_zero, add_zero]
case e_M.h.e_6.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (fun i j =>
      vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
        (↑(Fin.succAbove 0) i)) =
    fun i j => (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ det
      (↑of fun i j =>
        vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
          (↑(Fin.succAbove 0) i)) =
    det (↑of fun i j => (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k))
congr
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin n
⊢ vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j)) (↑(Fin.succAbove 0) i) =
    (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)
case e_M.h.e_6.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (fun i j =>
      vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j))
        (↑(Fin.succAbove 0) i)) =
    fun i j => (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)
ext (i j)
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin n
⊢ v (Fin.succ i) ^ (↑j + 1) - v 0 ^ (↑j + 1) =
    (∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) * (v (Fin.succ i) - v 0)
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin n
⊢ vecCons (v 0 ^ ↑(Fin.succ j)) (fun i => v (Fin.succ i) ^ ↑(Fin.succ j) - v 0 ^ ↑(Fin.succ j)) (↑(Fin.succAbove 0) i) =
    (v (Fin.succ i) - v 0) * ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)
rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm]
no goals
case e_M.h.e_6.h.h.h
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin n
⊢ v (Fin.succ i) ^ (↑j + 1) - v 0 ^ (↑j + 1) =
    (∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) * (v (Fin.succ i) - v 0)
exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    ∏ i : Fin (Nat.succ n), ∏ j in Ioi i, (v j - v i)
simp_rw [Fin.prod_univ_succ, Fin.prod_Ioi_zero, Fin.prod_Ioi_succ]
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
h : (det fun i j => (v ∘ Fin.succ) i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, ((v ∘ Fin.succ) j - (v ∘ Fin.succ) i)
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
have h := ih (v ∘ Fin.succ)
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
h : (det fun i j => v (Fin.succ i) ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v (Fin.succ j) - v (Fin.succ i))
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
h : (det fun i j => (v ∘ Fin.succ) i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, ((v ∘ Fin.succ) j - (v ∘ Fin.succ) i)
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
unfold Function.comp at h
no goals
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
h : (det fun i j => v (Fin.succ i) ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v (Fin.succ j) - v (Fin.succ i))
⊢ ((∏ i : Fin n, (v (Fin.succ i) - v 0)) * det fun i j => v (Fin.succ i) ^ ↑j) =
    (∏ j : Fin n, (v (Fin.succ j) - v 0)) * ∏ x : Fin n, ∏ j in Ioi x, (v (Fin.succ j) - v (Fin.succ x))
rw [h]
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ ↑of (fun i j => v i ^ ↑j) i j =
    ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) i j +
      vecCons 0 1 i * ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) 0 j
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ ∀ (i j : Fin (Nat.succ n)),
    ↑of (fun i j => v i ^ ↑j) i j =
      ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) i j +
        vecCons 0 1 i * ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) 0 j
intro i j
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v i ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i +
      vecCons 0 1 i * vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) 0
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ ↑of (fun i j => v i ^ ↑j) i j =
    ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) i j +
      vecCons 0 1 i * ↑of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i) 0 j
simp_rw [of_apply]
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v i ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i + vecCons 0 1 i * v 0 ^ ↑j
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v i ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i +
      vecCons 0 1 i * vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) 0
rw [Matrix.cons_val_zero]
case succ.calc_1.refine'_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v 0 ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) 0 + vecCons 0 1 0 * v 0 ^ ↑j

case succ.calc_1.refine'_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ v (Fin.succ i) ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) (Fin.succ i) + vecCons 0 1 (Fin.succ i) * v 0 ^ ↑j
case succ.calc_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v i ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) i + vecCons 0 1 i * v 0 ^ ↑j
refine' Fin.cases _ (fun i => _) i
case succ.calc_1.refine'_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ v (Fin.succ i) ^ ↑j = v (Fin.succ i) ^ ↑j - v 0 ^ ↑j + 1 * v 0 ^ ↑j
case succ.calc_1.refine'_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ v (Fin.succ i) ^ ↑j =
    vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) (Fin.succ i) + vecCons 0 1 (Fin.succ i) * v 0 ^ ↑j
rw [Matrix.cons_val_succ, Matrix.cons_val_succ, Pi.one_apply]
no goals
case succ.calc_1.refine'_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i✝ j : Fin (Nat.succ n)
i : Fin n
⊢ v (Fin.succ i) ^ ↑j = v (Fin.succ i) ^ ↑j - v 0 ^ ↑j + 1 * v 0 ^ ↑j
ring
no goals
case succ.calc_1.refine'_1
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
i j : Fin (Nat.succ n)
⊢ v 0 ^ ↑j = vecCons (v 0 ^ ↑j) (fun i => v (Fin.succ i) ^ ↑j - v 0 ^ ↑j) 0 + vecCons 0 1 0 * v 0 ^ ↑j
simp
case succ.calc_2.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
ih : ∀ (v : Fin Nat.zero → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin Nat.zero, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ Nat.zero) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j

case succ.calc_2.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
case succ.calc_2
R : Type u_1
inst✝ : CommRing R
n✝ : ℕ
v✝ : Fin n✝ → R
n : ℕ
ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ n) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
cases n
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ ∀ (i : Fin (n✝ + 1)), ∑ k in range (↑0 + 1), v (Fin.succ i) ^ k * v 0 ^ (↑0 - k) = v (Fin.succ i) ^ ↑0

case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ ∀ (i : Fin (n✝ + 1)) (j : Fin n✝),
    ∑ k in range (↑(Fin.succ j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.succ j) - k) =
      v (Fin.succ i) ^ ↑(Fin.succ j) +
        v 0 * ∑ k in range (↑(↑Fin.castSucc j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(↑Fin.castSucc j) - k)
case succ.calc_2.succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
apply det_eq_of_forall_col_eq_smul_add_pred fun _ => v 0
no goals
case succ.calc_2.zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
ih : ∀ (v : Fin Nat.zero → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin Nat.zero, ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ Nat.zero) → R
⊢ (det fun i j => ∑ k in range (↑j + 1), v (Fin.succ i) ^ k * v 0 ^ (↑j - k)) = det fun i j => v (Fin.succ i) ^ ↑j
rw [det_eq_one_of_card_eq_zero (Fintype.card_fin 0),
det_eq_one_of_card_eq_zero (Fintype.card_fin 0)]
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
j : Fin (n✝ + 1)
⊢ ∑ k in range (↑0 + 1), v (Fin.succ j) ^ k * v 0 ^ (↑0 - k) = v (Fin.succ j) ^ ↑0
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ ∀ (i : Fin (n✝ + 1)), ∑ k in range (↑0 + 1), v (Fin.succ i) ^ k * v 0 ^ (↑0 - k) = v (Fin.succ i) ^ ↑0
intro j
no goals
case succ.calc_2.succ.A_zero
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
j : Fin (n✝ + 1)
⊢ ∑ k in range (↑0 + 1), v (Fin.succ j) ^ k * v 0 ^ (↑0 - k) = v (Fin.succ j) ^ ↑0
simp
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ k in range (↑(Fin.succ j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.succ j) - k) =
    v (Fin.succ i) ^ ↑(Fin.succ j) +
      v 0 * ∑ k in range (↑(↑Fin.castSucc j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(↑Fin.castSucc j) - k)
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
⊢ ∀ (i : Fin (n✝ + 1)) (j : Fin n✝),
    ∑ k in range (↑(Fin.succ j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.succ j) - k) =
      v (Fin.succ i) ^ ↑(Fin.succ j) +
        v 0 * ∑ k in range (↑(↑Fin.castSucc j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(↑Fin.castSucc j) - k)
intro i j
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x in range (↑j + 1 + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    v (Fin.succ i) ^ (↑j + 1) + v 0 * ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j - x)
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ k in range (↑(Fin.succ j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(Fin.succ j) - k) =
    v (Fin.succ i) ^ ↑(Fin.succ j) +
      v 0 * ∑ k in range (↑(↑Fin.castSucc j) + 1), v (Fin.succ i) ^ k * v 0 ^ (↑(↑Fin.castSucc j) - k)
simp only [smul_eq_mul, Pi.add_apply, Fin.val_succ, Fin.coe_castSucc, Pi.smul_apply]
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ v (Fin.succ i) ^ (↑j + 1) + ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    v (Fin.succ i) ^ (↑j + 1) + ∑ x in range (↑j + 1), v 0 * (v (Fin.succ i) ^ x * v 0 ^ (↑j - x))
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x in range (↑j + 1 + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    v (Fin.succ i) ^ (↑j + 1) + v 0 * ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j - x)
rw [Finset.sum_range_succ, add_comm, tsub_self, pow_zero, mul_one, Finset.mul_sum]
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    ∑ x in range (↑j + 1), v 0 * (v (Fin.succ i) ^ x * v 0 ^ (↑j - x))
case succ.calc_2.succ.A_succ
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ v (Fin.succ i) ^ (↑j + 1) + ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    v (Fin.succ i) ^ (↑j + 1) + ∑ x in range (↑j + 1), v 0 * (v (Fin.succ i) ^ x * v 0 ^ (↑j - x))
congr 1
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ v (Fin.succ i) ^ i' * v 0 ^ (↑j + 1 - i') = v 0 * (v (Fin.succ i) ^ i' * v 0 ^ (↑j - i'))
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
⊢ ∑ x in range (↑j + 1), v (Fin.succ i) ^ x * v 0 ^ (↑j + 1 - x) =
    ∑ x in range (↑j + 1), v 0 * (v (Fin.succ i) ^ x * v 0 ^ (↑j - x))
refine' Finset.sum_congr rfl fun i' hi' => _
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ i' ≤ ↑j
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ v (Fin.succ i) ^ i' * v 0 ^ (↑j + 1 - i') = v 0 * (v (Fin.succ i) ^ i' * v 0 ^ (↑j - i'))
rw [mul_left_comm (v 0), Nat.succ_sub, pow_succ]
no goals
case succ.calc_2.succ.A_succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
v✝ : Fin n → R
n✝ : ℕ
ih : ∀ (v : Fin (Nat.succ n✝) → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin (Nat.succ n✝), ∏ j in Ioi i, (v j - v i)
v : Fin (Nat.succ (Nat.succ n✝)) → R
i : Fin (n✝ + 1)
j : Fin n✝
i' : ℕ
hi' : i' ∈ range (↑j + 1)
⊢ i' ≤ ↑j
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp hi')