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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
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
p1 : P
hp1 : p1 ∈ s
p2 p : P
⊢ p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
rw [← mem_coe] at hp1
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1) ↔
    ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
rw [← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp1)),
  direction_affineSpan_insert hp1, Submodule.mem_sup]
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1) →
    ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ 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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0) →
    ∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1) ↔
    ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
constructor
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v1 : V
hv1 : v1 ∈ Submodule.span k {p2 -ᵥ p1}
v2 : V
hv2 : v2 ∈ direction s
hp : v1 + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1) →
    ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
rintro ⟨v1, hv1, v2, hv2, hp⟩
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v1 : V
hv1 : ∃ a, a • (p2 -ᵥ p1) = v1
v2 : V
hv2 : v2 ∈ direction s
hp : v1 + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v1 : V
hv1 : v1 ∈ Submodule.span k {p2 -ᵥ p1}
v2 : V
hv2 : v2 ∈ direction s
hp : v1 + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
rw [Submodule.mem_span_singleton] at hv1
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : r • (p2 -ᵥ p1) + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v1 : V
hv1 : ∃ a, a • (p2 -ᵥ p1) = v1
v2 : V
hv2 : v2 ∈ direction s
hp : v1 + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
rcases hv1 with ⟨r, rfl⟩
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : r • (p2 -ᵥ p1) + v2 = p -ᵥ p1
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : r • (p2 -ᵥ p1) + v2 = p -ᵥ p1
⊢ ∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0
use r, v2 +ᵥ p1, vadd_mem_of_mem_direction hv2 hp1
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : p -ᵥ p1 = r • (p2 -ᵥ p1) + v2
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : r • (p2 -ᵥ p1) + v2 = p -ᵥ p1
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
symm at hp
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp✝ : p -ᵥ p1 = r • (p2 -ᵥ p1) + v2
hp : p = r • (p2 -ᵥ p1) + v2 +ᵥ p1
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp : p -ᵥ p1 = r • (p2 -ᵥ p1) + v2
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp
no goals
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
v2 : V
hv2 : v2 ∈ direction s
r : k
hp✝ : p -ᵥ p1 = r • (p2 -ᵥ p1) + v2
hp : p = r • (p2 -ᵥ p1) + v2 +ᵥ p1
⊢ p = r • (p2 -ᵥ p1) +ᵥ (v2 +ᵥ p1)
rw [hp, vadd_vadd]
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
p1 : P
hp1 : p1 ∈ ↑s
p2 : P
r : k
p3 : P
hp3 : p3 ∈ s
⊢ ∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = r • (p2 -ᵥ p1) +ᵥ p3 -ᵥ p1
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
p1 : P
hp1 : p1 ∈ ↑s
p2 p : P
⊢ (∃ r p0 _hp0, p = r • (p2 -ᵥ p1) +ᵥ p0) →
    ∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = p -ᵥ p1
rintro ⟨r, p3, hp3, rfl⟩
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
p1 : P
hp1 : p1 ∈ ↑s
p2 : P
r : k
p3 : P
hp3 : p3 ∈ s
⊢ r • (p2 -ᵥ p1) + (p3 -ᵥ p1) = r • (p2 -ᵥ p1) +ᵥ p3 -ᵥ p1
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
p1 : P
hp1 : p1 ∈ ↑s
p2 : P
r : k
p3 : P
hp3 : p3 ∈ s
⊢ ∃ y, y ∈ Submodule.span k {p2 -ᵥ p1} ∧ ∃ z, z ∈ direction s ∧ y + z = r • (p2 -ᵥ p1) +ᵥ p3 -ᵥ p1
use r • (p2 -ᵥ p1), Submodule.mem_span_singleton.2 ⟨r, rfl⟩, p3 -ᵥ p1,
  vsub_mem_direction hp3 hp1
no goals
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
p1 : P
hp1 : p1 ∈ ↑s
p2 : P
r : k
p3 : P
hp3 : p3 ∈ s
⊢ r • (p2 -ᵥ p1) + (p3 -ᵥ p1) = r • (p2 -ᵥ p1) +ᵥ p3 -ᵥ p1
rw [vadd_vsub_assoc, add_comm]