case h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p x : P
⊢ x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
⊢ ↑(affineSpan k {p}) = {p}
ext x
case h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}
case h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p x : P
⊢ x ∈ ↑(affineSpan k {p}) ↔ x ∈ {p}
rw [mem_coe, ← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_singleton p)) _,
  direction_affineSpan]
no goals
case h
k : Type u_2
V : Type u_3
P : Type u_1
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p x : P
⊢ x -ᵥ p ∈ vectorSpan k {p} ↔ x ∈ {p}
simp