k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
have hv : vectorSpan k (insert p₁ s) = vectorSpan k ({p₁, p₂, p₃} : Set P) := by
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
  symm
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]
no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
hv : vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
⊢ Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
rw [Collinear, Collinear, hv]
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ direction (affineSpan k (insert p₁ ↑(affineSpan k s))) = vectorSpan k {p₁, p₂, p₃}
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ vectorSpan k (insert p₁ s) = vectorSpan k {p₁, p₂, p₃}
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan]
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ vectorSpan k {p₁, p₂, p₃} = direction (affineSpan k (insert p₁ ↑(affineSpan k s)))
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ direction (affineSpan k (insert p₁ ↑(affineSpan k s))) = vectorSpan k {p₁, p₂, p₃}
symm
no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.318365
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Collinear k s
p₁ p₂ p₃ : P
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₃ : p₂ ≠ p₃
⊢ vectorSpan k {p₁, p₂, p₃} = direction (affineSpan k (insert p₁ ↑(affineSpan k s)))
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, h.affineSpan_eq_of_ne hp₂ hp₃ hp₂p₃]