-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
/-- When the affine space is also a vector space, the affine span is contained within the linear
span. -/
lemma affineSpan_le_toAffineSubspace_span {s : Set V} :
    affineSpan k s ≤ (Submodule.span k s).toAffineSubspace

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
c : k
u : V
hu✝ : u ∈ affineSpan k s
v : V
hv✝ : v ∈ affineSpan k s
w : V
hw✝ : w ∈ affineSpan k s
hu : u ∈ Submodule.span k s
hv : v ∈ Submodule.span k s
hw : w ∈ Submodule.span k s
⊢ c • (u - v) ∈ Submodule.span k s

Tactic:
exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Result:
no goals

Proof state:
case mem
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x✝ x : V
hx : x ∈ s
⊢ x ∈ Submodule.span k s

Tactic:
exact Submodule.subset_span hx

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ ↑(affineSpan k s)
⊢ x ∈ Submodule.span k s

Tactic:
induction hx using affineSpan_induction' with
| mem x hx => exact Submodule.subset_span hx
| smul_vsub_vadd c u _ v _ w _ hu hv hw =>
  simp only [vsub_eq_sub, vadd_eq_add]
  apply Submodule.add_mem _ _ hw
  exact Submodule.smul_mem _ _ (Submodule.sub_mem _ hu hv)

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ ↑(affineSpan k s)
⊢ x ∈ ↑(Submodule.span k s).toAffineSubspace

Tactic:
simp only [SetLike.mem_coe, Submodule.mem_toAffineSubspace]

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ ↑(affineSpan k s)
⊢ x ∈ Submodule.span k s

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ affineSpan k s ≤ (Submodule.span k s).toAffineSubspace

Tactic:
intro x hx

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
hx : x ∈ ↑(affineSpan k s)
⊢ x ∈ ↑(Submodule.span k s).toAffineSubspace

Proof state:
case smul_vsub_vadd
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
c : k
u : V
hu✝ : u ∈ affineSpan k s
v : V
hv✝ : v ∈ affineSpan k s
w : V
hw✝ : w ∈ affineSpan k s
hu : u ∈ Submodule.span k s
hv : v ∈ Submodule.span k s
hw : w ∈ Submodule.span k s
⊢ c • (u - v) + w ∈ Submodule.span k s

Tactic:
apply Submodule.add_mem _ _ hw

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
c : k
u : V
hu✝ : u ∈ affineSpan k s
v : V
hv✝ : v ∈ affineSpan k s
w : V
hw✝ : w ∈ affineSpan k s
hu : u ∈ Submodule.span k s
hv : v ∈ Submodule.span k s
hw : w ∈ Submodule.span k s
⊢ c • (u - v) ∈ Submodule.span k s

Proof state:
case smul_vsub_vadd
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
c : k
u : V
hu✝ : u ∈ affineSpan k s
v : V
hv✝ : v ∈ affineSpan k s
w : V
hw✝ : w ∈ affineSpan k s
hu : u ∈ Submodule.span k s
hv : v ∈ Submodule.span k s
hw : w ∈ Submodule.span k s
⊢ c • (u -ᵥ v) +ᵥ w ∈ Submodule.span k s

Tactic:
simp only [vsub_eq_sub, vadd_eq_add]

Result:
case smul_vsub_vadd
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
x : V
c : k
u : V
hu✝ : u ∈ affineSpan k s
v : V
hv✝ : v ∈ affineSpan k s
w : V
hw✝ : w ∈ affineSpan k s
hu : u ∈ Submodule.span k s
hv : v ∈ Submodule.span k s
hw : w ∈ Submodule.span k s
⊢ c • (u - v) + w ∈ Submodule.span k s