𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
⊢ StarConvex 𝕜 x s
intro y hy a b ha hb hab
case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ∈ s

case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ∈ s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
obtain hxy | hyx := h _ hy
case inl.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ x ≤ a • x + b • y

case inl.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ≤ y
case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ∈ s
refine' hs.out hx hy (mem_Icc.2 ⟨_, _⟩)
case inl.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ≤ y
case inl.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ x ≤ a • x + b • y

case inl.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ 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 inl.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ 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_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • x ≤ a • x + b • y
gcongr
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ≤ a • y + b • y
gcongr
case inr.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ y ≤ a • x + b • y

case inr.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ≤ x
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ∈ s
refine' hs.out hy hx (mem_Icc.2 ⟨_, _⟩)
case inr.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ≤ x
case inr.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ y ≤ a • x + b • y

case inr.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ≤ x
calc
  y = a • y + b • y := (Convex.combo_self hab _).symm
  _ ≤ a • x + b • y := by gcongr
no goals
case inr.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ≤ x
calc
  a • x + b • y ≤ a • x + b • x := by gcongr
  _ = x := Convex.combo_self hab _
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • y + b • y ≤ a • x + b • y
gcongr
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.162524
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x : E
s : Set E
hs : OrdConnected s
hx : x ∈ s
h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ≤ a • x + b • x
gcongr