-- Mathlib/Analysis/Convex/Segment.lean
theorem Convex.mem_Ioc (h : x < y) :
    z ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Proof state:
case refine_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 * x + b * y ∈ Ioc x y

Tactic:
rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
hz : z ∈ Ioc x y
⊢ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)

Result:
case refine_1.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

Proof state:
case refine_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
exact (hz.1.ne rfl).elim

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

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

Result:
case refine_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

case refine_1.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
hb' : 0 < b
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

Proof state:
case refine_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 * x + b * y ∈ Ioc x y

Tactic:
rw [zero_add] at hab

Result:
case refine_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 * x + b * y ∈ Ioc x y

Proof state:
case refine_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
rw [hab, one_mul, zero_mul, add_zero] at hz

Result:
case refine_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Proof state:
case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ioc x y

Tactic:
rintro ⟨a, b, ha, hb, hab, rfl⟩

Result:
case refine_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a * x + b * y ∈ Ioc x y

Proof state:
case refine_1.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a * x + b * y ∈ Ioc x y
hb' : 0 < b
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

Tactic:
exact ⟨a, b, ha, hb', hab, rfl⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ z ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Tactic:
refine ⟨fun hz => ?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
hz : z ∈ Ioc x y
⊢ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

case refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
h : x < y
⊢ (∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z) → z ∈ Ioc x y

Proof state:
case refine_2.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a * x + b * y ∈ Ioc x y

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

Result:
case refine_2.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
b : 𝕜
hb : 0 < b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 * x + b * y ∈ Ioc x y

case refine_2.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y

Proof state:
case refine_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a + 0 = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
rw [add_zero] at hab

Result:
case refine_1.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : a * x + 0 * y ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Proof state:
case refine_2.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y

Tactic:
exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)

Result:
no goals