-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
K : Type u_2
inst : Field K
n : ℕ
v w : Fin n → K
zero : ∀ (v w : Fin 0 → K), (projVandermonde v w).det = ∏ i : Fin 0, ∏ j ∈ Ioi i, (v j * w i - v i * w j)
succ :
  ∀ (n : ℕ) (ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j))
    (v w : Fin (n + 1) → K), (projVandermonde v w).det = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j * w i - v i * w j)
⊢ (projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j * w i - v i * w j)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
  /- We can assume not all `w i` are zero, and therefore that `w 0 ≠ 0`,
  since otherwise we can swap row `0` with another nonzero row. -/
  wlog h0 : w 0 ≠ 0 generalizing v w with aux
  · obtain h0' | ⟨i₀, hi₀ : w i₀ ≠ 0⟩ := forall_or_exists_not (w · = 0)
    · obtain rfl | hne := eq_or_ne n 0
      · simp [projVandermonde_apply]
      rw [det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),
        Finset.prod_sigma', Finset.prod_eq_zero (i := ⟨0, Fin.last n⟩) (by simpa) (by simp [h0'])]
    rw [← mul_right_inj' (a := ((Equiv.swap 0 i₀).sign : K))
      (by simp [show 0 ≠ i₀ by rintro rfl; contradiction]), ← det_permute, ← projVandermonde_comp,
      aux _ _ (by simpa), ← (Equiv.swap 0 i₀).prod_Ioi_comp_eq_sign_mul_prod (by simp)]
    rfl
  /- Let `W` be obtained from the matrix by subtracting `r = (v 0) / (w 0)` times each column
  from the next column, starting from the penultimate column. This doesn't change the determinant.-/
  set r := v 0 / w 0 with hr
  set W : Matrix (Fin (n + 1)) (Fin (n + 1)) K := .of fun i ↦ (cons (projVandermonde v w i 0)
    (fun j ↦ projVandermonde v w i j.succ - r * projVandermonde v w i j.castSucc))
  -- deleting the first row and column of `W` gives a row-scaling of a Vandermonde matrix.
  have hW_eq : (W.submatrix succ succ) = .of fun i j ↦ (v (succ i) - r * w (succ i)) *
      projVandermonde (v ∘ succ) (w ∘ succ) i j := by
    ext i j
    simp only [projVandermonde_apply, val_zero, rev_zero, val_last, val_succ,
      val_castSucc, submatrix_apply, Function.comp_apply, rev_succ,
      W, r, rev_castSucc]
    simp
    ring
  /- The first row of `W` is `[(w 0)^n, 0, ..., 0]` - take a cofactor expansion along this row,
  and apply induction. -/
  rw [det_eq_of_forall_col_eq_smul_add_pred (B := W) (c := fun _ ↦ r) (by simp [W])
    (fun i j ↦ by simp [W, r, projVandermonde_apply]), det_succ_row_zero,
    Finset.sum_eq_single 0 _ (by simp)]
  · rw [succAbove_zero, hW_eq, det_mul_column, ih]
    simp only [Nat.succ_eq_add_one, coe_ofNat_eq_mod, Nat.zero_mod,
      pow_zero, show W 0 0 = w 0 ^ n by simp [W, projVandermonde_apply], one_mul, hr]
    field_simp
    simp only [Finset.prod_div_distrib, Finset.prod_const, Finset.card_fin, Function.comp_apply]
    field_simp
    simp only [prod_univ_succ, Ioi_zero_eq_map, Finset.prod_map, coe_succEmb, prod_Ioi_succ]
  intro j _ hj0
  obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero hj0
  rw [mul_eq_zero, mul_eq_zero]
  refine .inl (.inr ?_)
  simp only [of_apply, projVandermonde_apply_of_ne_zero h0, val_succ, val_castSucc, cons_succ, W, r]
  ring

Premises used: Fin.coe_succEmb, Matrix.det_permute, Fin.cons_succ, Nat.succ_eq_add_one, Fin.succ, Matrix, Fin.val_succ, Matrix.of_apply, Finset.prod_const, mul_eq_zero, Fin.prod_Ioi_succ, Finset.sum_eq_single, pow_zero, Fin.prod_univ_succ, HAdd.hAdd, Finset.card_fin, Matrix.det_mul_column, Finset.prod_eq_zero, Finset.prod_sigma', forall_or_exists_not, Fin.coe_ofNat_eq_mod, eq_or_ne, Function.comp_apply, Nat.zero_mod, Matrix.det_eq_zero_of_column_eq_zero, Matrix.projVandermonde_apply, Finset.prod_map, Matrix.projVandermonde_comp, Fin.succAbove_zero, OfNat.ofNat, Fin.Ioi_zero_eq_map, Fin, Matrix.det_succ_row_zero, Eq, Matrix.zero, Finset.prod_div_distrib, one_mul, Fin.val_castSucc, rfl