case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
⊢ p ∈ s1 ↔ p ∈ s2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
⊢ s1 = s2
ext p
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
⊢ p ∈ s1 ↔ p ∈ s2
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
⊢ p ∈ s1 ↔ p ∈ s2
have hq1 := Set.mem_of_mem_inter_left hn.some_mem
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s1 ↔ p ∈ s2
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
⊢ p ∈ s1 ↔ p ∈ s2
have hq2 := Set.mem_of_mem_inter_right hn.some_mem
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s1 → p ∈ s2

case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s2 → p ∈ s1
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s1 ↔ p ∈ s2
constructor
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p ∈ s2
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s1 → p ∈ s2
intro hp
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn +ᵥ Set.Nonempty.some hn ∈ s2
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p ∈ s2
rw [← vsub_vadd p hn.some]
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s2
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn +ᵥ Set.Nonempty.some hn ∈ s2
refine' vadd_mem_of_mem_direction _ hq2
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s1
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s2
rw [← hd]
no goals
case h.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s1
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s1
exact vsub_mem_direction hp hq1
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p ∈ s1
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
⊢ p ∈ s2 → p ∈ s1
intro hp
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn +ᵥ Set.Nonempty.some hn ∈ s1
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p ∈ s1
rw [← vsub_vadd p hn.some]
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s1
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn +ᵥ Set.Nonempty.some hn ∈ s1
refine' vadd_mem_of_mem_direction _ hq1
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s2
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s1
rw [hd]
no goals
case h.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s1 s2 : AffineSubspace k P
hd : direction s1 = direction s2
hn : Set.Nonempty (↑s1 ∩ ↑s2)
p : P
hq1 : Set.Nonempty.some hn ∈ ↑s1
hq2 : Set.Nonempty.some hn ∈ ↑s2
hp : p ∈ s2
⊢ p -ᵥ Set.Nonempty.some hn ∈ direction s2
exact vsub_mem_direction hp hq2