-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem mem_affineSpan_insert_iff {s : AffineSubspace k P} {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ p : P) :
    p ∈ affineSpan k (insert p₂ (s : Set P)) ↔
      ∃ r : k, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁ : V) +ᵥ p0

Proof state:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0) → ∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = p -ᵥ p₁

Tactic:
rintro ⟨r, p₃, hp₃, rfl⟩

Result:
case mpr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ ∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = p -ᵥ p₁) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
constructor

Result:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = p -ᵥ p₁) → ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0) → ∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = p -ᵥ p₁

Proof state:
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₁ : V
hv₁ : v₁ ∈ Submodule.span k {p₂ -ᵥ p₁}
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rw [Submodule.mem_span_singleton] at hv₁

Result:
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₁ : V
hv₁ : ∃ a, a • (p₂ -ᵥ p₁) = v₁
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Proof state:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Tactic:
symm at hp

Result:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Proof state:
case mpr.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ ∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Tactic:
use r • (p₂ -ᵥ p₁), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p₃ -ᵥ p₁,
  vsub_mem_direction hp₃ hp₁

Result:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Proof state:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
r : k
p₃ : P
hp₃ : p₃ ∈ s
⊢ r • (p₂ -ᵥ p₁) + (p₃ -ᵥ p₁) = (r • (p₂ -ᵥ p₁) +ᵥ p₃) -ᵥ p₁

Tactic:
rw [vadd_vsub_assoc]

Result:
no goals

Proof state:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Tactic:
rw [hp, vadd_vadd]

Result:
no goals

Proof state:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Tactic:
rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp

Result:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p = (r • (p₂ -ᵥ p₁) + v₂) +ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Proof state:
case mp.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁

Result:
case right
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Proof state:
case mp.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₁ : V
hv₁ : ∃ a, a • (p₂ -ᵥ p₁) = v₁
v₂ : V
hv₂ : v₂ ∈ s.direction
hp : v₁ + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rcases hv₁ with ⟨r, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : r • (p₂ -ᵥ p₁) + v₂ = p -ᵥ p₁
⊢ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp₁)),
  direction_affineSpan_insert hp₁, Submodule.mem_sup]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ y ∈ Submodule.span k {p₂ -ᵥ p₁}, ∃ z ∈ s.direction, y + z = p -ᵥ p₁) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0