Why does this apply not work?

Stream: new members

[Abdullah Uyu]

import Mathlib.LinearAlgebra.LinearIndependent

variable [DivisionRing K] [AddCommGroup V] [Module K V]

theorem lin_dep_aab (a b : V) : ¬ LinearIndependent K ![a, a, b] := by
intro aab_dep
rw [linearIndependent_iff'] at aab_dep
have aab_comb : (Finset.sum {0, 1, 2} fun i ↦ ![1, -1, 0] i • ![a, a, b] i) = 0 := by simp
apply (aab_dep {0, 1, 2} ![1, -1, 0]) at aab_comb

fails with

Failed to find (Finset.sum {0, 1, 2} fun i => ![1, -1, 0] i • ![a, a, b] i) =
  0 as the type of a parameter of (Finset.sum {0, 1, 2} fun i => ![1, -1, 0] i • ![a, a, b] i) = 0 →
  ∀ i ∈ {0, 1, 2}, ![1, -1, 0] i = 0.

I am trying to eventually get an obvious contradiction here.

[Abdullah Uyu]

In other words, I want to instantiate aab_dep for {0,1,2} and ![1,-1,0].

[Abdullah Uyu]

Oh, I am doing something silly.

[Abdullah Uyu]

Well, nevermind. I still don't understand what's going on here.

[Abdullah Uyu]

FWIW, the following works:

theorem lin_dep_aab (a b : V) : ¬ LinearIndependent K ![a, a, b] := by
intro aab_dep
rw [linearIndependent_iff'] at aab_dep
specialize aab_dep {0, 1, 2} ![1, -1, 0]
aesop

But, I suppose aesopis an overkill for this.