Lean4
/-- Alternative definition of the direction when the affine subspace is nonempty. This is defined so
that the order on submodules (as used in the definition of `Submodule.span`) can be used in the
proof of `coe_direction_eq_vsub_set`, and is not intended to be used beyond that proof. -/
def directionOfNonempty {s : AffineSubspace k P} (h : (s : Set P).Nonempty) : Submodule k V
where
carrier := (s : Set P) -ᵥ s
zero_mem' := by
obtain ⟨p, hp⟩ := h
exact vsub_self p ▸ vsub_mem_vsub hp hp
add_mem' := by
rintro _ _ ⟨p₁, hp₁, p₂, hp₂, rfl⟩ ⟨p₃, hp₃, p₄, hp₄, rfl⟩
rw [← vadd_vsub_assoc]
refine vsub_mem_vsub ?_ hp₄
convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp₃
rw [one_smul]
smul_mem' := by
rintro c _ ⟨p₁, hp₁, p₂, hp₂, rfl⟩
rw [← vadd_vsub (c • (p₁ -ᵥ p₂)) p₂]
refine vsub_mem_vsub ?_ hp₂
exact s.smul_vsub_vadd_mem c hp₁ hp₂ hp₂
