case intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 : P
hp2 : p2 ∈ spanPoints k s
p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 : P
hp1 : p1 ∈ spanPoints k s
hp2 : p2 ∈ spanPoints k s
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
rcases hp1 with ⟨p1a, ⟨hp1a, ⟨v1, ⟨hv1, hv1p⟩⟩⟩⟩
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
case intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 : P
hp2 : p2 ∈ spanPoints k s
p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
rcases hp2 with ⟨p2a, ⟨hp2a, ⟨v2, ⟨hv2, hv2p⟩⟩⟩⟩
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ p1 -ᵥ p2 ∈ vectorSpan k s
rw [hv1p, hv2p, vsub_vadd_eq_vsub_sub (v1 +ᵥ p1a), vadd_vsub_assoc, add_comm, add_sub_assoc]
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
hv1v2 : v1 - v2 ∈ vectorSpan k s
⊢ p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
have hv1v2 : v1 - v2 ∈ vectorSpan k s := by
  rw [sub_eq_add_neg]
  apply (vectorSpan k s).add_mem hv1
  rw [← neg_one_smul k v2]
  exact (vectorSpan k s).smul_mem (-1 : k) hv2
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
hv1v2 : v1 - v2 ∈ vectorSpan k s
⊢ p1a -ᵥ p2a ∈ vectorSpan k s
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
hv1v2 : v1 - v2 ∈ vectorSpan k s
⊢ p1a -ᵥ p2a + (v1 - v2) ∈ vectorSpan k s
refine' (vectorSpan k s).add_mem _ hv1v2
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
hv1v2 : v1 - v2 ∈ vectorSpan k s
⊢ p1a -ᵥ p2a ∈ vectorSpan k s
exact vsub_mem_vectorSpan k hp1a hp2a
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ v1 + -v2 ∈ vectorSpan k s
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ v1 - v2 ∈ vectorSpan k s
rw [sub_eq_add_neg]
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ -v2 ∈ vectorSpan k s
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ v1 + -v2 ∈ vectorSpan k s
apply (vectorSpan k s).add_mem hv1
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ -1 • v2 ∈ vectorSpan k s
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ -v2 ∈ vectorSpan k s
rw [← neg_one_smul k v2]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p1 p2 p1a : P
hp1a : p1a ∈ s
v1 : V
hv1 : v1 ∈ vectorSpan k s
hv1p : p1 = v1 +ᵥ p1a
p2a : P
hp2a : p2a ∈ s
v2 : V
hv2 : v2 ∈ vectorSpan k s
hv2p : p2 = v2 +ᵥ p2a
⊢ -1 • v2 ∈ vectorSpan k s
exact (vectorSpan k s).smul_mem (-1 : k) hv2