feat: add Basis.flag_le_ker_dual (#11265)

From sphere-eversion; I adapted the proof to mathlib's definition and golfed it a bit.
This adds a new import; as this file is not imported anywhere, this seems fine.

Author: grunweg

Mathlib/Data/Fin/Basic.lean

@@ -1082,6 +1082,9 @@ theorem coe_eq_castSucc {a : Fin n} : (a : Fin (n + 1)) = castSucc a := by
   exact val_cast_of_lt (Nat.lt.step a.is_lt)
 #align fin.coe_eq_cast_succ Fin.coe_eq_castSucc
 
+theorem coe_succ_lt_iff_lt {n : ℕ} {j k : Fin n} : (j : Fin <| n + 1) < k ↔ j < k := by
+  simp only [coe_eq_castSucc]; rfl
+
 #align fin.coe_succ_eq_succ Fin.coeSucc_eq_succ
 
 #align fin.lt_succ Fin.lt_succ

Mathlib/LinearAlgebra/Basis/Flag.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Patrick Massot
 -/
 import Mathlib.LinearAlgebra.Basis
+import Mathlib.LinearAlgebra.Dual
 import Mathlib.Data.Fin.FlagRange
 
 /-!
@@ -79,6 +80,11 @@ theorem flag_le_ker_coord (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n}
   nontriviality R
   exact b.flag_le_ker_coord_iff.2 h
 
+theorem flag_le_ker_dual (b : Basis (Fin n) R M) (k : Fin n) :
+    b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k) := by
+  nontriviality R
+  rw [coe_dualBasis, b.flag_le_ker_coord_iff]
+
 end CommRing
 
 section DivisionRing