no goals
R : Type u_1
V : Type u_2
V' : Type u_4
P : Type u_3
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing 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
f : P →ᵃ[R] P'
hf : Function.Injective ↑f
⊢ SOppSide (map f s) (↑f x) (↑f y) ↔ SOppSide s x y
simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]