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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
⊢ ∃ p, ↑s1 ∩ ↑s2 = {p}
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
hd : IsCompl (direction s1) (direction s2)
⊢ ∃ p, ↑s1 ∩ ↑s2 = {p}
cases' inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top with p hp
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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
⊢ ↑s1 ∩ ↑s2 = {p}
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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
⊢ ∃ p, ↑s1 ∩ ↑s2 = {p}
use p
case intro.h
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 ↔ q ∈ {p}
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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
⊢ ↑s1 ∩ ↑s2 = {p}
ext q
case intro.h
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 ↔ q = p
case intro.h
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 ↔ q ∈ {p}
rw [Set.mem_singleton_iff]
case intro.h.mp
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 → q = p

case intro.h.mpr
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q = p → q ∈ ↑s1 ∩ ↑s2
case intro.h
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 ↔ q = p
constructor
case intro.h.mp.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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
hq1 : q ∈ ↑s1
hq2 : q ∈ ↑s2
⊢ q = p
case intro.h.mp
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q ∈ ↑s1 ∩ ↑s2 → q = p
rintro ⟨hq1, hq2⟩
case intro.h.mp.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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
hq1 : q ∈ ↑s1
hq2 : q ∈ ↑s2
hqp : q -ᵥ p ∈ direction s1 ⊓ direction s2
⊢ q = p
case intro.h.mp.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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
hq1 : q ∈ ↑s1
hq2 : q ∈ ↑s2
⊢ q = p
have hqp : q -ᵥ p ∈ s1.direction ⊓ s2.direction :=
  ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
no goals
case intro.h.mp.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
h1 : Set.Nonempty ↑s1
h2 : Set.Nonempty ↑s2
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
hq1 : q ∈ ↑s1
hq2 : q ∈ ↑s2
hqp : q -ᵥ p ∈ direction s1 ⊓ direction s2
⊢ q = p
rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp
no goals
case intro.h.mpr
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
hd : IsCompl (direction s1) (direction s2)
p : P
hp : p ∈ ↑s1 ∩ ↑s2
q : P
⊢ q = p → q ∈ ↑s1 ∩ ↑s2
exact fun h => h.symm ▸ hp