case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.73157
G : Type ?u.73160
ι : Type ?u.73163
π : ι → Type ?u.73168
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.73157
G : Type ?u.73160
ι : Type ?u.73163
π : ι → Type ?u.73168
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
⊢ [x-[𝕜]y] = (fun θ => x + θ • (y - x)) '' Icc 0 1
convert segment_eq_image 𝕜 x y using 2
case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.73157
G : Type ?u.73160
ι : Type ?u.73163
π : ι → Type ?u.73168
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.73157
G : Type ?u.73160
ι : Type ?u.73163
π : ι → Type ?u.73168
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + a✝¹ • (y - x) = (1 - a✝¹) • x + a✝¹ • y
simp only [smul_sub, sub_smul, one_smul]
no goals
case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.73157
G : Type ?u.73160
ι : Type ?u.73163
π : ι → Type ?u.73168
inst✝⁵ : OrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : AddCommGroup G
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ x + (a✝¹ • y - a✝¹ • x) = x - a✝¹ • x + a✝¹ • y
abel