R : Type u_1
V : Type u_2
V' : Type ?u.453341
P : Type u_3
P' : Type ?u.453347
inst✝⁶ : LinearOrderedField R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : ¬y ∈ s
h : x = y
⊢ y ∈ s
R : Type u_1
V : Type u_2
V' : Type ?u.453341
P : Type u_3
P' : Type ?u.453347
inst✝⁶ : LinearOrderedField R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : ¬y ∈ s
⊢ SOppSide s y (↑(pointReflection R x) y)
refine' (sbtw_pointReflection_of_ne R fun h => hy _).sOppSide_of_not_mem_of_mem hy hx
no goals
R : Type u_1
V : Type u_2
V' : Type ?u.453341
P : Type u_3
P' : Type ?u.453347
inst✝⁶ : LinearOrderedField R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
hx : x ∈ s
hy : ¬y ∈ s
h : x = y
⊢ y ∈ s
rwa [← h]