k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
rw [vectorSpan_def]
case refine'_1
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)

case refine'_2
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ (fun x x_1 => x -ᵥ x_1) p '' s ⊆ s -ᵥ s
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) = Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
refine' le_antisymm _ (Submodule.span_mono _)
case refine'_1
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ s -ᵥ s ⊆ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
case refine'_1
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s)
rw [Submodule.span_le]
case refine'_1.intro.intro.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p1 p2 = v
⊢ v ∈ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
case refine'_1
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ s -ᵥ s ⊆ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
rintro v ⟨p1, p2, hp1, hp2, hv⟩
case refine'_1.intro.intro.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p -ᵥ p2 - (p -ᵥ p1) = v
⊢ v ∈ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
case refine'_1.intro.intro.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p1 p2 = v
⊢ v ∈ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
simp_rw [← vsub_sub_vsub_cancel_left p1 p2 p] at hv
case refine'_1.intro.intro.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p -ᵥ p2 - (p -ᵥ p1) = v
⊢ ∀ (p_1 : Submodule k V), (fun x x_1 => x -ᵥ x_1) p '' s ⊆ ↑p_1 → p -ᵥ p2 - (p -ᵥ p1) ∈ p_1
case refine'_1.intro.intro.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p -ᵥ p2 - (p -ᵥ p1) = v
⊢ v ∈ ↑(Submodule.span k ((fun x x_1 => x -ᵥ x_1) p '' s))
rw [← hv, SetLike.mem_coe, Submodule.mem_span]
no goals
case refine'_1.intro.intro.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p1 p2 : P
hp1 : p1 ∈ s
hp2 : p2 ∈ s
hv : p -ᵥ p2 - (p -ᵥ p1) = v
⊢ ∀ (p_1 : Submodule k V), (fun x x_1 => x -ᵥ x_1) p '' s ⊆ ↑p_1 → p -ᵥ p2 - (p -ᵥ p1) ∈ p_1
exact fun m hm => Submodule.sub_mem _ (hm ⟨p2, hp2, rfl⟩) (hm ⟨p1, hp1, rfl⟩)
case refine'_2.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p2 : P
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p p2 = v
⊢ v ∈ s -ᵥ s
case refine'_2
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
⊢ (fun x x_1 => x -ᵥ x_1) p '' s ⊆ s -ᵥ s
rintro v ⟨p2, hp2, hv⟩
no goals
case refine'_2.intro.intro
k : Type u_3
V : Type u_2
P : Type u_1
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.250908
s : Set P
p : P
hp : p ∈ s
v : V
p2 : P
hp2 : p2 ∈ s
hv : (fun x x_1 => x -ᵥ x_1) p p2 = v
⊢ v ∈ s -ᵥ s
exact ⟨p, p2, hp, hp2, hv⟩