case inl
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ (p : P), p ∈ ∅ → ∃ r, p = r • v +ᵥ p₀

case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ Collinear k s ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)
no goals
case inl
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ (p : P), p ∈ ∅ → ∃ r, p = r • v +ᵥ p₀
simp [collinear_empty]
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁) ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
rw [collinear_iff_of_mem hp₁]
case inr.intro.mp
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁) → ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀

case inr.intro.mpr
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀) → ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
case inr.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁) ↔ ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
constructor
no goals
case inr.intro.mp
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁) → ∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀
exact fun h => ⟨p₁, h⟩
case inr.intro.mpr.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
⊢ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
case inr.intro.mpr
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ p₀ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₀) → ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
rintro ⟨p, v, hv⟩
case inr.intro.mpr.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
⊢ ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
case inr.intro.mpr.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
⊢ ∃ v, ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
use v
case inr.intro.mpr.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁
case inr.intro.mpr.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
⊢ ∀ (p : P), p ∈ s → ∃ r, p = r • v +ᵥ p₁
intro p₂ hp₂
case inr.intro.mpr.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ p₁
case inr.intro.mpr.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁
rcases hv p₂ hp₂ with ⟨r, rfl⟩
case inr.intro.mpr.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ (r₁ • v +ᵥ p)
case inr.intro.mpr.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ p₁
rcases hv p₁ hp₁ with ⟨r₁, rfl⟩
case inr.intro.mpr.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ r • v +ᵥ p = (r - r₁) • v +ᵥ (r₁ • v +ᵥ p)
case inr.intro.mpr.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ (r₁ • v +ᵥ p)
use r - r₁
no goals
case inr.intro.mpr.intro.intro.intro.intro
k : Type u_2
V : Type u_3
P : Type u_1
ι : Type ?u.258453
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ (p_1 : P), p_1 ∈ s → ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
r₁ : k
hp₁ : r₁ • v +ᵥ p ∈ s
⊢ r • v +ᵥ p = (r - r₁) • v +ᵥ (r₁ • v +ᵥ p)
simp [vadd_vadd, ← add_smul]