case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ Ioo x y
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
⊢ openSegment 𝕜 x y ⊆ Ioo x y
rintro z ⟨a, b, ha, hb, hab, rfl⟩
case intro.intro.intro.intro.intro.left
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a • x + b • y

case intro.intro.intro.intro.intro.right
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ Ioo x y
constructor
case intro.intro.intro.intro.intro.right
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
case intro.intro.intro.intro.intro.left
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a • x + b • y

case intro.intro.intro.intro.intro.right
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
calc
  x = a • x + b • x := (Convex.combo_self hab _).symm
  _ < a • x + b • y := by gcongr
no goals
case intro.intro.intro.intro.intro.right
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < y
calc
  a • x + b • y < a • y + b • y := by gcongr
  _ = y := Convex.combo_self hab _
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • x < a • x + b • y
gcongr
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.250125
G : Type ?u.250128
ι : Type ?u.250131
π : ι → Type ?u.250136
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y < a • y + b • y
gcongr