-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_eq_span_vsub_set_left {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((p -ᵥ ·) '' s)

Proof state:
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 : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x => p -ᵥ x) '' s)

Tactic:
rw [vectorSpan_def]

Result:
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 : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x => p -ᵥ x) '' s)

Proof state:
case refine_1
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 : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x => p -ᵥ x) '' s)

Tactic:
rw [Submodule.span_le]

Result:
case refine_1
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 : Set P
p : P
hp : p ∈ s
⊢ s -ᵥ s ⊆ ↑(Submodule.span k ((fun x => p -ᵥ x) '' s))

Proof state:
case refine_1.intro.intro.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun x1 x2 => x1 -ᵥ x2) p₁ p₂ = v
⊢ v ∈ ↑(Submodule.span k ((fun x => p -ᵥ x) '' s))

Tactic:
simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv

Result:
case refine_1.intro.intro.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ v ∈ ↑(Submodule.span k ((fun x => p -ᵥ x) '' s))

Proof state:
case refine_1
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 : Set P
p : P
hp : p ∈ s
⊢ s -ᵥ s ⊆ ↑(Submodule.span k ((fun x => p -ᵥ x) '' s))

Tactic:
rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩

Result:
case refine_1.intro.intro.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun x1 x2 => x1 -ᵥ x2) p₁ p₂ = v
⊢ v ∈ ↑(Submodule.span k ((fun x => p -ᵥ x) '' s))

Proof state:
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 : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x => p -ᵥ x) '' s)

Tactic:
refine le_antisymm ?_ (Submodule.span_mono ?_)

Result:
case refine_1
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 : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x => p -ᵥ x) '' s)

case refine_2
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 : Set P
p : P
hp : p ∈ s
⊢ (fun x => p -ᵥ x) '' s ⊆ s -ᵥ s

Proof state:
case refine_1.intro.intro.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ ∀ (p_1 : Submodule k V), (fun x => p -ᵥ x) '' s ⊆ ↑p_1 → p -ᵥ p₂ - (p -ᵥ p₁) ∈ p_1

Tactic:
exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)

Result:
no goals

Proof state:
case refine_2
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 : Set P
p : P
hp : p ∈ s
⊢ (fun x => p -ᵥ x) '' s ⊆ s -ᵥ s

Tactic:
rintro v ⟨p₂, hp₂, hv⟩

Result:
case refine_2.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun x => p -ᵥ x) p₂ = v
⊢ v ∈ s -ᵥ s

Proof state:
case refine_1.intro.intro.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ v ∈ ↑(Submodule.span k ((fun x => p -ᵥ x) '' s))

Tactic:
rw [← hv, SetLike.mem_coe, Submodule.mem_span]

Result:
case refine_1.intro.intro.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ ∀ (p_1 : Submodule k V), (fun x => p -ᵥ x) '' s ⊆ ↑p_1 → p -ᵥ p₂ - (p -ᵥ p₁) ∈ p_1

Proof state:
case refine_2.intro.intro
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 : Set P
p : P
hp : p ∈ s
v : V
p₂ : P
hp₂ : p₂ ∈ s
hv : (fun x => p -ᵥ x) p₂ = v
⊢ v ∈ s -ᵥ s

Tactic:
exact ⟨p, hp, p₂, hp₂, hv⟩

Result:
no goals