case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ direction s = ⊤ → s = ⊤

case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ s = ⊤ → direction s = ⊤
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
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ direction s = ⊤ ↔ s = ⊤
constructor
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = ⊤
⊢ s = ⊤
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ direction s = ⊤ → s = ⊤
intro hd
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = direction ⊤
⊢ s = ⊤
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = ⊤
⊢ s = ⊤
rw [← direction_top k V P] at hd
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = direction ⊤
⊢ Set.Nonempty (↑s ∩ ↑⊤)
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = direction ⊤
⊢ s = ⊤
refine' ext_of_direction_eq hd _
no goals
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
hd : direction s = direction ⊤
⊢ Set.Nonempty (↑s ∩ ↑⊤)
simp [h]
case 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
h : Set.Nonempty ↑⊤
⊢ direction ⊤ = ⊤
case 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
s : AffineSubspace k P
h : Set.Nonempty ↑s
⊢ s = ⊤ → direction s = ⊤
rintro rfl
no goals
case 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
h : Set.Nonempty ↑⊤
⊢ direction ⊤ = ⊤
simp