-- 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.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

Tactic:
simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
  hw₁, one_smul, hg]

Result:
no goals

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
ι : 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
⊢ ∑ i : ι × κ, w i.1 * v i.2 = 1

Tactic:
rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]

Result:
no goals

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 ∈ (convexHull R) s
hy : y ∈ (convexHull R) t
⊢ (x, y) ∈ (convexHull R) (s ×ˢ t)

Tactic:
rw [mem_convexHull_iff_exists_fintype] at hx hy ⊢

Result:
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)

Proof state:
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)

Tactic:
obtain ⟨κ, _, v, g, hv₀, hv₁, hgt, hg⟩ := hy

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
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)