case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x y → x = y

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x = y → x ∈ openSegment 𝕜 x y
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x y ↔ x = y
constructor
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
a b : 𝕜
w✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ x = y
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x y → x = y
rintro ⟨a, b, _, hb, hab, hx⟩
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
a b : 𝕜
w✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ a • x + (fun x x_1 => x • x_1) b x = a • x + (fun x x_1 => x • x_1) b y
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
a b : 𝕜
w✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ x = y
refine' smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 _)
no goals
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
a b : 𝕜
w✝ : 0 < a
hb : 0 < b
hab : a + b = 1
hx : a • x + b • y = x
⊢ a • x + (fun x x_1 => x • x_1) b x = a • x + (fun x x_1 => x • x_1) b y
rw [hx, ← add_smul, hab, one_smul]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x x
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x = y → x ∈ openSegment 𝕜 x y
rintro rfl
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ {x}
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ openSegment 𝕜 x x
rw [openSegment_same]
no goals
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.172150
G : Type ?u.172153
ι : Type ?u.172156
π : ι → Type ?u.172161
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ x ∈ {x}
exact mem_singleton _