no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.51667
G : Type ?u.51670
ι : Type ?u.51673
π : ι → Type ?u.51678
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
x✝ : z ∈ openSegment 𝕜 x x
a b : 𝕜
w✝¹ : 0 < a
w✝ : 0 < b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}
simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.51667
G : Type ?u.51670
ι : Type ?u.51673
π : ι → Type ?u.51678
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.51667
G : Type ?u.51670
ι : Type ?u.51673
π : ι → Type ?u.51678
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
⊢ z ∈ openSegment 𝕜 x x
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.51667
G : Type ?u.51670
ι : Type ?u.51673
π : ι → Type ?u.51678
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ a • x + (1 - a) • x = z
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.51667
G : Type ?u.51670
ι : Type ?u.51673
π : ι → Type ?u.51678
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x
refine' ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, _⟩
no goals
case intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.51667
G : Type ?u.51670
ι : Type ?u.51673
π : ι → Type ?u.51678
inst✝⁷ : OrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ a • x + (1 - a) • x = z
rw [← add_smul, add_sub_cancel'_right, one_smul, h]