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 : direction s1 ⊔ direction s2 = ⊤
h : ¬Set.Nonempty (↑s1 ∩ ↑s2)
⊢ False
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 : direction s1 ⊔ direction s2 = ⊤
⊢ Set.Nonempty (↑s1 ∩ ↑s2)
by_contra 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 : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
⊢ False
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 : direction s1 ⊔ direction s2 = ⊤
h : ¬Set.Nonempty (↑s1 ∩ ↑s2)
⊢ False
rw [Set.not_nonempty_iff_eq_empty] at 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 : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
hlt : direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
⊢ False
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 : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
⊢ False
have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 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 : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
hlt : ⊤ < direction (s1 ⊔ s2)
⊢ False
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 : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
hlt : direction s1 ⊔ direction s2 < direction (s1 ⊔ s2)
⊢ False
rw [hd] at hlt
no goals
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 : direction s1 ⊔ direction s2 = ⊤
h : ↑s1 ∩ ↑s2 = ∅
hlt : ⊤ < direction (s1 ⊔ s2)
⊢ False
exact not_top_lt hlt