k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h : ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ affineSpan k {p₁, p₂}
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
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₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ affineSpan k {p₁, p₂}
rw [collinear_iff_of_mem hp₁] at h
case intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
⊢ p₃ ∈ affineSpan k {p₁, p₂}
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
h : ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ p₃ ∈ affineSpan k {p₁, p₂}
rcases h with ⟨v, h⟩
case intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₃ : P
hp₁ : p₁ ∈ s
hp₃ : p₃ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
⊢ p₃ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
case intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
⊢ p₃ ∈ affineSpan k {p₁, p₂}
rcases h p₂ hp₂ with ⟨r₂, rfl⟩
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₃ • v +ᵥ p₁ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
case intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₃ : P
hp₁ : p₁ ∈ s
hp₃ : p₃ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
⊢ p₃ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
rcases h p₃ hp₃ with ⟨r₃, rfl⟩
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ ∃ r, r • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₃ • v +ᵥ p₁ ∈ affineSpan k {p₁, r₂ • v +ᵥ p₁}
rw [vadd_left_mem_affineSpan_pair]
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ (r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ ∃ r, r • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
refine' ⟨r₃ / r₂, _⟩
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
h₂ : r₂ ≠ 0
⊢ (r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ (r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
have h₂ : r₂ ≠ 0 := by
  rintro rfl
  simp at hp₁p₂
no goals
case intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
h₂ : r₂ ≠ 0
⊢ (r₃ / r₂) • (r₂ • v +ᵥ p₁ -ᵥ p₁) = r₃ • v
simp [smul_smul, h₂]
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
hp₂ : 0 • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ 0 • v +ᵥ p₁
⊢ False
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₂ : k
hp₂ : r₂ • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ r₂ • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
⊢ r₂ ≠ 0
rintro rfl
no goals
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.310342
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
v : V
h : ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
r₃ : k
hp₃ : r₃ • v +ᵥ p₁ ∈ s
hp₂ : 0 • v +ᵥ p₁ ∈ s
hp₁p₂ : p₁ ≠ 0 • v +ᵥ p₁
⊢ False
simp at hp₁p₂