-- Mathlib/Analysis/Convex/Star.lean
/-- If `x < y`, then `(Set.Iic x)ᶜ` is star convex at `y`. -/
lemma starConvex_compl_Iic (h : x < y) : StarConvex 𝕜 y (Iic x)ᶜ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ z ≤ x

Tactic:
refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ b • z < b • x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ (a + b) • x - a • y < b • x

Tactic:
rw [add_smul, sub_lt_iff_lt_add']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ a • x + b • x < a • y + b • x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ a • x + b • x < a • y + b • x

Tactic:
gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ b • z < b • x

Tactic:
calc
  b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
  _ < b • x := by
    rw [add_smul, sub_lt_iff_lt_add']
    gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
⊢ StarConvex 𝕜 y (Iic x)ᶜ

Tactic:
refine (starConvex_iff_forall_pos <| by simp [h.not_le]).mpr fun z hz a b ha hb hab ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
hz : z ∈ (Iic x)ᶜ
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + b • z ∈ (Iic x)ᶜ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
hz : ¬z ≤ x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ¬a • y + b • z ≤ x

Tactic:
contrapose! hz

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ z ≤ x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
hz : z ∈ (Iic x)ᶜ
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + b • z ∈ (Iic x)ᶜ

Tactic:
rw [mem_compl_iff, mem_Iic] at hz ⊢

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
hz : ¬z ≤ x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ¬a • y + b • z ≤ x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ b • z ≤ (a + b) • x - a • y

Tactic:
rwa [le_sub_iff_add_le', hab, one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedRing 𝕜
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x < y
⊢ y ∈ (Iic x)ᶜ

Tactic:
simp [h.not_le]

Result:
no goals