-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_Iio (r : β) : Convex 𝕜 (Iio r)

Proof state:
case inl
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r

Tactic:
rwa [zero_smul, zero_add, hab, one_smul]

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Tactic:
rw [mem_Iio] at hx hy

Result:
case inr
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Proof state:
case inr
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Tactic:
calc
  a • x + b • y < a • r + b • r := add_lt_add_of_lt_of_le
      (smul_lt_smul_of_pos_left hx ha') (smul_le_smul_of_nonneg_left hy.le hb)
  _ = r := Convex.combo_self hab _

Result:
no goals

Proof state:
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r : β
⊢ Convex 𝕜 (Iio r)

Tactic:
intro x hx y hy a b ha hb hab

Result:
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r

Proof state:
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Result:
case inl
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r

case inr
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r

Proof state:
case inl
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r

Tactic:
rw [zero_add] at hab

Result:
case inl
𝕜 : Type u_1
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r