k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ Submodule.span k ((fun x x_1 => x -ᵥ x_1) (p i₀) '' (p '' (univ \ {i₀}))) =
    Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
rw [← Set.image_univ, vectorSpan_image_eq_span_vsub_set_left_ne k _ (Set.mem_univ i₀)]
case e_s.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ v ∈ (fun x x_1 => x -ᵥ x_1) (p i₀) '' (p '' (univ \ {i₀})) ↔ v ∈ range fun i => p i₀ -ᵥ p ↑i
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ Submodule.span k ((fun x x_1 => x -ᵥ x_1) (p i₀) '' (p '' (univ \ {i₀}))) =
    Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
congr with v
case e_s.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) ↔ ∃ a h, p i₀ -ᵥ p a = v
case e_s.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ v ∈ (fun x x_1 => x -ᵥ x_1) (p i₀) '' (p '' (univ \ {i₀})) ↔ v ∈ range fun i => p i₀ -ᵥ p ↑i
simp only [Set.mem_range, Set.mem_image, Set.mem_diff, Set.mem_singleton_iff, Subtype.exists,
  Subtype.coe_mk]
case e_s.h.mp
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) → ∃ a h, p i₀ -ᵥ p a = v

case e_s.h.mpr
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ a h, p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v
case e_s.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) ↔ ∃ a h, p i₀ -ᵥ p a = v
constructor
case e_s.h.mp.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
i₁ : ι
left✝ : i₁ ∈ univ
hi₁ : ¬i₁ = i₀
hv : p i₀ -ᵥ p i₁ = v
⊢ ∃ a h, p i₀ -ᵥ p a = v
case e_s.h.mp
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) → ∃ a h, p i₀ -ᵥ p a = v
rintro ⟨x, ⟨i₁, ⟨⟨_, hi₁⟩, rfl⟩⟩, hv⟩
no goals
case e_s.h.mp.intro.intro.intro.intro.intro
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
i₁ : ι
left✝ : i₁ ∈ univ
hi₁ : ¬i₁ = i₀
hv : p i₀ -ᵥ p i₁ = v
⊢ ∃ a h, p i₀ -ᵥ p a = v
exact ⟨i₁, hi₁, hv⟩
no goals
case e_s.h.mpr
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ a h, p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v
exact fun ⟨i₁, hi₁, hv⟩ => ⟨p i₁, ⟨i₁, ⟨Set.mem_univ _, hi₁⟩, rfl⟩, hv⟩