case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162050
G : Type ?u.162053
ι : Type ?u.162056
π : ι → Type ?u.162061
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162050
G : Type ?u.162053
ι : Type ?u.162056
π : ι → Type ?u.162061
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x ∈ [x - y-[𝕜]x + y]
convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _
no goals
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162050
G : Type ?u.162053
ι : Type ?u.162056
π : ι → Type ?u.162061
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x✝ y✝ : E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)
rw [midpoint_sub_add]