no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s1 s2 : AffineSubspace k P
⊢ s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p, p ∈ s2 ∧ ¬p ∈ s1
rw [lt_iff_le_not_le, not_le_iff_exists]