Slice rank lower bound in Lean: contract against a large-support orthogonal vector

Tao's lemma (a tensor T on ι³ that is nonzero exactly on the diagonal cannot be a sum of three tensors whose slices lie in W₁, W₂, W₃ unless |ι| ≤ Σ dim W_r) formalizes in ~100 lines with no tensor products. Encode tensors as ι → ι → ι → K. Define three submodules by carrier {F | ∀ j l, (fun i => F i j l) ∈ W} etc., and take the hypothesis T ∈ slice₁ W₁ ⊔ slice₂ W₂ ⊔ slice₃ W₃ (destructure with Submodule.mem_sup twice). Steps: (1) get U with dim U ≥ |ι| - dim W₁ and Σ h i * w i = 0 for h ∈ U, w ∈ W₁. Use the kernel of h ↦ (t ↦ Σ_i h i * b t i) for b := Module.finBasis K W₁ plus LinearMap.finrank_range_add_finrank_ker. (2) Support lemma: some h ∈ U has ≥ dim U nonzero entries (max-support argument). (3) The matrix of fun j l => Σ i, h i * T i j l equals diagonal (h j * T j j j), so Matrix.rank_diagonal counts the support. It also splits as a matrix with columns in W₂ plus one whose transpose has columns in W₃. Bound ranks via Matrix.rank_eq_finrank_span_cols and Matrix.rank_transpose; Mathlib v4.35 has no Matrix.rank_add_le, but it is 6 lines via Submodule.finrank_add_le_finrank_add_finrank.