-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_iff_exists_forall_eq_smul_vadd (s : Set P) :
    Collinear k s ↔ ∃ (p₀ : P) (v : V), ∀ p ∈ s, ∃ r : k, p = r • v +ᵥ p₀

Proof state:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ p ∈ ∅, ∃ r, p = r • v +ᵥ p₀

Tactic:
simp [collinear_empty]

Result:
no goals

Proof state:
case inr.intro.mpr
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p = r • v +ᵥ p₀) → ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁

Tactic:
rintro ⟨p, v, hv⟩

Result:
case inr.intro.mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
⊢ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁

Proof state:
case inr.intro.mpr.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
⊢ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁

Tactic:
use v

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
⊢ ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ 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

Tactic:
simp [vadd_vadd, ← add_smul]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)

Result:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ p ∈ ∅, ∃ r, p = r • v +ᵥ p₀

case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p = r • v +ᵥ p₀

Proof state:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁) ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
constructor

Result:
case inr.intro.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁) → ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

case inr.intro.mpr
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p = r • v +ᵥ p₀) → ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁

Tactic:
rcases hv p₂ hp₂ with ⟨r, rfl⟩

Result:
case h.intro
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ p₁

Proof state:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
rw [collinear_iff_of_mem hp₁]

Result:
case inr.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁) ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Proof state:
case h.intro
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
r : k
hp₂ : r • v +ᵥ p ∈ s
⊢ ∃ r_1, r • v +ᵥ p = r_1 • v +ᵥ p₁

Tactic:
rcases hv p₁ hp₁ with ⟨r₁, rfl⟩

Result:
case h.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ 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

Proof state:
case h.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ 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

Tactic:
use r - r₁

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
v : V
hv : ∀ 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

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
⊢ ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁

Tactic:
intro p₂ hp₂

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
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 ∈ s, ∃ r, p_1 = r • v +ᵥ p
p₂ : P
hp₂ : p₂ ∈ s
⊢ ∃ r, p₂ = r • v +ᵥ p₁

Proof state:
case inr.intro.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ : P
hp₁ : p₁ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₁) → ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
exact fun h => ⟨p₁, h⟩

Result:
no goals