case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = 0 → ∃ i j, v i = v j ∧ i ≠ j

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → det (vandermonde v) = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = 0 ↔ ∃ i j, v i = v j ∧ i ≠ j
constructor
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x : Fin n), (x ∈ univ ∧ ∃ a, a ∈ Ioi x ∧ v a = v x) → ∃ i j, v i = v j ∧ i ≠ j
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ det (vandermonde v) = 0 → ∃ i j, v i = v j ∧ i ≠ j
simp only [det_vandermonde v, Finset.prod_eq_zero_iff, sub_eq_zero, forall_exists_index]
case mp.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i : Fin n
left✝ : i ∈ univ
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ i j, v i = v j ∧ i ≠ j
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x : Fin n), (x ∈ univ ∧ ∃ a, a ∈ Ioi x ∧ v a = v x) → ∃ i j, v i = v j ∧ i ≠ j
rintro i ⟨_, j, h₁, h₂⟩
no goals
case mp.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i : Fin n
left✝ : i ∈ univ
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ i j, v i = v j ∧ i ≠ j
exact ⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → det (vandermonde v) = 0
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → det (vandermonde v) = 0
simp only [Ne.def, forall_exists_index, and_imp]
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → det (vandermonde v) = 0
refine' fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => _)
no goals
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k
rw [vandermonde_apply, vandermonde_apply, h₁]