R : Type u_2
V : Type u_3
V' : Type ?u.631338
P : Type u_1
P' : Type ?u.631344
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ Sbtw R x (midpoint R x y) y
R : Type u_2
V : Type u_3
V' : Type ?u.631338
P : Type u_1
P' : Type ?u.631344
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ Sbtw R x (midpoint R x y) y
have h : midpoint R x y ≠ x := by simp [h]
case h.e'_10
R : Type u_2
V : Type u_3
V' : Type ?u.631338
P : Type u_1
P' : Type ?u.631344
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ y = ↑(pointReflection R (midpoint R x y)) x
R : Type u_2
V : Type u_3
V' : Type ?u.631338
P : Type u_1
P' : Type ?u.631344
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ Sbtw R x (midpoint R x y) y
convert sbtw_pointReflection_of_ne R h
no goals
case h.e'_10
R : Type u_2
V : Type u_3
V' : Type ?u.631338
P : Type u_1
P' : Type ?u.631344
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h✝ : x ≠ y
h : midpoint R x y ≠ x
⊢ y = ↑(pointReflection R (midpoint R x y)) x
rw [pointReflection_midpoint_left]
no goals
R : Type u_2
V : Type u_3
V' : Type ?u.631338
P : Type u_1
P' : Type ?u.631344
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : x ≠ y
⊢ midpoint R x y ≠ x
simp [h]