case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h2 : Set.Nonempty ↑s2
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
he : ↑s1 ∩ ↑s2 = ∅
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
cases' h1 with p1 hp1
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
h2 : Set.Nonempty ↑s2
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
cases' h2 with p2 hp2
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ direction s1 ⊔ direction s2 ≤ direction (s1 ⊔ s2) ∧ ∃ x, x ∈ direction (s1 ⊔ s2) ∧ ¬x ∈ direction s1 ⊔ direction s2
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
rw [SetLike.lt_iff_le_and_exists]
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ ¬p2 -ᵥ p1 ∈ direction s1 ⊔ direction s2
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ direction s1 ⊔ direction s2 ≤ direction (s1 ⊔ s2) ∧ ∃ x, x ∈ direction (s1 ⊔ s2) ∧ ¬x ∈ direction s1 ⊔ direction s2
use sup_direction_le s1 s2, p2 -ᵥ p1,
  vsub_mem_direction ((le_sup_right : s2 ≤ s1 ⊔ s2) hp2) ((le_sup_left : s1 ≤ s1 ⊔ s2) hp1)
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
h : p2 -ᵥ p1 ∈ direction s1 ⊔ direction s2
⊢ False
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
⊢ ¬p2 -ᵥ p1 ∈ direction s1 ⊔ direction s2
intro h
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
h : ∃ y, y ∈ direction s1 ∧ ∃ z, z ∈ direction s2 ∧ y + z = p2 -ᵥ p1
⊢ False
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
h : p2 -ᵥ p1 ∈ direction s1 ⊔ direction s2
⊢ False
rw [Submodule.mem_sup] at h
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2 : v1 + v2 = p2 -ᵥ p1
⊢ False
case intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
h : ∃ y, y ∈ direction s1 ∧ ∃ z, z ∈ direction s2 ∧ y + z = p2 -ᵥ p1
⊢ False
rcases h with ⟨v1, hv1, v2, hv2, hv1v2⟩
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ False
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2 : v1 + v2 = p2 -ᵥ p1
⊢ False
rw [← sub_eq_zero, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm v1, add_assoc, ←
  vadd_vsub_assoc, ← neg_neg v2, add_comm, ← sub_eq_add_neg, ← vsub_vadd_eq_vsub_sub,
  vsub_eq_zero_iff_eq] at hv1v2
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ Set.Nonempty (↑s1 ∩ ↑s2)
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ False
refine' Set.Nonempty.ne_empty _ he
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ v1 +ᵥ p1 ∈ ↑s2
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ Set.Nonempty (↑s1 ∩ ↑s2)
use v1 +ᵥ p1, vadd_mem_of_mem_direction hv1 hp1
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ -v2 +ᵥ p2 ∈ ↑s2
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ v1 +ᵥ p1 ∈ ↑s2
rw [hv1v2]
no goals
case intro.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
S : AffineSpace V P
p₁ p₂ : P
s1 s2 : AffineSubspace k P
he : ↑s1 ∩ ↑s2 = ∅
p1 : P
hp1 : p1 ∈ ↑s1
p2 : P
hp2 : p2 ∈ ↑s2
v1 : V
hv1 : v1 ∈ direction s1
v2 : V
hv2 : v2 ∈ direction s2
hv1v2✝ : v1 + v2 = p2 -ᵥ p1
hv1v2 : v1 +ᵥ p1 = -v2 +ᵥ p2
⊢ -v2 +ᵥ p2 ∈ ↑s2
exact vadd_mem_of_mem_direction (Submodule.neg_mem _ hv2) hp2