-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_assoc_aux (s t u : Set E) :
    convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ 0
hab₂ : a₂ + 0 = 1
⊢ a₁ • x + b₁ • y = a₂ • (a₁ • x + b₁ • y) + 0 • z

Tactic:
linear_combination (norm := module) -hab₂ • (a₁ • x + b₁ • y)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ 0
hab₂ : a₂ + 0 = 1
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + 0 • z ∈ segment 𝕜 a b

Tactic:
refine ⟨x, hx, y, ⟨y, hy, z, hz, left_mem_segment 𝕜 _ _⟩, a₁, b₁, ha₁, hb₁, hab₁, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ 0
hab₂ : a₂ + 0 = 1
⊢ a₁ • x + b₁ • y = a₂ • (a₁ • x + b₁ • y) + 0 • z

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ convexJoin 𝕜 (convexJoin 𝕜 s t) u ⊆ convexJoin 𝕜 s (convexJoin 𝕜 t u)

Tactic:
simp_rw [subset_def, mem_convexJoin]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ ∀ (x : E),
    (∃ a, (∃ a_1 ∈ s, ∃ b ∈ t, a ∈ segment 𝕜 a_1 b) ∧ ∃ b ∈ u, x ∈ segment 𝕜 a b) →
      ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ x ∈ segment 𝕜 a b

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ b₂ / (a₂ * b₁ + b₂)

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b

Tactic:
refine
  ⟨x, hx, (a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z,
    ⟨y, hy, z, hz, _, _, by positivity, by positivity, by field_simp, rfl⟩,
    a₂ * a₁, a₂ * b₁ + b₂, by positivity, by positivity, ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.refine_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ a₂ * a₁ + (a₂ * b₁ + b₂) = 1

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr.refine_2
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ (a₂ * a₁) • x + (a₂ * b₁ + b₂) • ((a₂ * b₁ / (a₂ * b₁ + b₂)) • y + (b₂ / (a₂ * b₁ + b₂)) • z) =
    a₂ • (a₁ • x + b₁ • y) + b₂ • z

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b

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

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ 0
hab₂ : a₂ + 0 = 1
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + 0 • z ∈ segment 𝕜 a b

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.inr
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ a₂ * b₁ + b₂

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂✝ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
hb₂ : 0 < b₂
⊢ 0 ≤ a₂ * a₁

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
⊢ ∀ (x : E),
    (∃ a, (∃ a_1 ∈ s, ∃ b ∈ t, a ∈ segment 𝕜 a_1 b) ∧ ∃ b ∈ u, x ∈ segment 𝕜 a b) →
      ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ x ∈ segment 𝕜 a b

Tactic:
rintro _ ⟨z, ⟨x, hx, y, hy, a₁, b₁, ha₁, hb₁, hab₁, rfl⟩, z, hz, a₂, b₂, ha₂, hb₂, hab₂, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t u : Set E
x : E
hx : x ∈ s
y : E
hy : y ∈ t
a₁ b₁ : 𝕜
ha₁ : 0 ≤ a₁
hb₁ : 0 ≤ b₁
hab₁ : a₁ + b₁ = 1
z : E
hz : z ∈ u
a₂ b₂ : 𝕜
ha₂ : 0 ≤ a₂
hb₂ : 0 ≤ b₂
hab₂ : a₂ + b₂ = 1
⊢ ∃ a ∈ s, ∃ b, (∃ a ∈ t, ∃ b_1 ∈ u, b ∈ segment 𝕜 a b_1) ∧ a₂ • (a₁ • x + b₁ • y) + b₂ • z ∈ segment 𝕜 a b