no goals
k : Type u_2
V : Type u_3
P : Type u_4
ι : Type u_1
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 2
⊢ AffineIndependent k p ↔ ¬finrank k { x // x ∈ vectorSpan k (Set.range p) } ≤ n
rw [affineIndependent_iff_le_finrank_vectorSpan k p hc, ← Nat.lt_iff_add_one_le, lt_iff_not_ge]