-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_affineSpan (s : Set P) : (affineSpan k s).direction = vectorSpan k s

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro.intro.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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ (fun x1 x2 => x1 -ᵥ x2) p₁ p₃ ∈ ↑(vectorSpan k s)

Tactic:
simp only [SetLike.mem_coe]

Result:
case a.intro.intro.intro.intro.intro.intro.intro.intro.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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ p₁ -ᵥ p₃ ∈ vectorSpan k 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
⊢ (affineSpan k s).direction = vectorSpan k s

Tactic:
apply le_antisymm

Result:
case a
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
⊢ (affineSpan k s).direction ≤ vectorSpan k s

case a
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
⊢ vectorSpan k s ≤ (affineSpan k s).direction

Proof state:
case a
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
⊢ vectorSpan k s ≤ (affineSpan k s).direction

Tactic:
exact vectorSpan_mono k (subset_spanPoints k s)

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro.intro.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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s

Tactic:
exact
  (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂

Result:
no goals

Proof state:
case a
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
⊢ (affineSpan k s).direction ≤ vectorSpan k s

Tactic:
refine Submodule.span_le.2 ?_

Result:
case a
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
⊢ ↑(affineSpan k s) -ᵥ ↑(affineSpan k s) ⊆ ↑(vectorSpan k s)

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro.intro.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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ p₁ -ᵥ p₃ ∈ vectorSpan k s

Tactic:
rw [hp₁, hp₃, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc]

Result:
case a.intro.intro.intro.intro.intro.intro.intro.intro.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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s

Proof state:
case a
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
⊢ ↑(affineSpan k s) -ᵥ ↑(affineSpan k s) ⊆ ↑(vectorSpan k s)

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

Result:
case a.intro.intro.intro.intro.intro.intro.intro.intro.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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ (fun x1 x2 => x1 -ᵥ x2) p₁ p₃ ∈ ↑(vectorSpan k s)