-- Mathlib/Analysis/Convex/Combination.lean
theorem mk_mem_convexHull_prod {t : Set F} {x : E} {y : F} (hx : x ∈ convexHull R s)
    (hy : y ∈ convexHull R t) : (x, y) ∈ convexHull R (s ×ˢ t)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)

Tactic:
refine ⟨ι × κ, inferInstance, fun p => w p.1 * v p.2, fun p ↦ (f p.1, g p.2),
  fun p ↦ mul_nonneg (hw₀ _) (hv₀ _), h_sum, fun p ↦ ⟨hfs _, hgt _⟩, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ ∑ i : ι × κ, (fun p => w p.1 * v p.2) i • (fun p => (f p.1, g p.2)) i = (x, y)

Proof state:
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
hx : ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x
hy : ∃ ι x w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)

Tactic:
obtain ⟨ι, _, w, f, hw₀, hw₁, hfs, hf⟩ := hx

Result:
case intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
hy : ∃ ι x w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y
ι : Type
w✝ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ ∑ i : ι × κ, (fun p => w p.1 * v p.2) i • (fun p => (f p.1, g p.2)) i = (x, y)

Tactic:
ext

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ (∑ i : ι × κ, (fun p => w p.1 * v p.2) i • (fun p => (f p.1, g p.2)) i).1 = (x, y).1

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.snd
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ (∑ i : ι × κ, (fun p => w p.1 * v p.2) i • (fun p => (f p.1, g p.2)) i).2 = (x, y).2

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.fst
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ (∑ i : ι × κ, (fun p => w p.1 * v p.2) i • (fun p => (f p.1, g p.2)) i).1 = (x, y).1

Tactic:
simp_rw [Prod.fst_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_comm (w _), mul_smul,
  sum_comm (γ := ι), ← Fintype.sum_smul_sum, hv₁, one_smul, hf]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)

Tactic:
have h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1 := by
  rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : LinearOrderedField R
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module R E
inst✝ : Module R F
s : Set E
t : Set F
x : E
y : F
ι : Type
w✝¹ : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w✝ : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : ∑ i : κ, v i = 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)