k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ directionOfNonempty h ≤ direction s
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ directionOfNonempty h = direction s
refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ ↑s -ᵥ ↑s ⊆ ↑(vectorSpan k ↑s)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ directionOfNonempty h ≤ direction s
rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk,
  AddSubmonoid.coe_set_mk]
no goals
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ ↑s -ᵥ ↑s ⊆ ↑(vectorSpan k ↑s)
exact (vsub_set_subset_vectorSpan k _)