case intro
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
⊢ direction ⊤ = ⊤
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
⊢ direction ⊤ = ⊤
cases' S.Nonempty with p
case intro.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
⊢ v ∈ direction ⊤ ↔ v ∈ ⊤
case intro
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
⊢ direction ⊤ = ⊤
ext v
case intro.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
_hv : v ∈ ⊤
⊢ v ∈ direction ⊤
case intro.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
⊢ v ∈ direction ⊤ ↔ v ∈ ⊤
refine' ⟨imp_intro Submodule.mem_top, fun _hv => _⟩
case intro.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
_hv : v ∈ ⊤
hpv : v +ᵥ p -ᵥ p ∈ direction ⊤
⊢ v ∈ direction ⊤
case intro.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
_hv : v ∈ ⊤
⊢ v ∈ direction ⊤
have hpv : (v +ᵥ p -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction :=
  vsub_mem_direction (mem_top k V _) (mem_top k V _)
no goals
case intro.h
k : Type u_2
V : Type u_1
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ p : P
v : V
_hv : v ∈ ⊤
hpv : v +ᵥ p -ᵥ p ∈ direction ⊤
⊢ v ∈ direction ⊤
rwa [vadd_vsub] at hpv