awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
⊢ Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
have refine_1 : Subset.{u_3} (α := Set E)
  {x : E |
    ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E),
      (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
  (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
Tactic: rw [_root_.convexHull_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ Membership.mem (γ := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E)) (t.centerMass w z)
have refine_1 : ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ s),
  Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑i : Set E) : Set E) (t.centerMass w z)
Tactic: simp only [mem_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ s),
    Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑i : Set E) : Set E) (t.centerMass w z)
have refine_1 : (↑(Finset.image z t) : Set E) ⊆ s
Tactic: refine ⟨t.image z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
refine_1 : (↑(Finset.image z t) : Set E) ⊆ s
⊢ ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ s),
    Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑i : Set E) : Set E) (t.centerMass w z)
have refine_1₁ : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑(Finset.image z t) : Set E) : Set E)
  (t.centerMass w z)
Tactic: refine ⟨t.image z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ (↑(Finset.image z t) : Set E) ⊆ s
have refine_1 : (↑t : Set ι) ⊆ z ⁻¹' s
Tactic: rw [coe_image, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑(Finset.image z t) : Set E) : Set E)
    (t.centerMass w z)
have refine_1 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
Tactic: apply t.centerMass_mem_convexHull hw₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
refine_1 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑(Finset.image z t) : Set E) : Set E)
    (t.centerMass w z)
have refine_1₁ : ∀ i ∈ t, z i ∈ (↑(Finset.image z t) : Set E)
Tactic: apply t.centerMass_mem_convexHull hw₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
have refine_1 : Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
  (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
Tactic: classical
  refine Subset.antisymm ?_ ?_
  · rw [_root_.convexHull_eq]
    rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    simp only [mem_iUnion]
    refine ⟨t.image z, ?_, ?_⟩
    · rw [coe_image, Set.image_subset_iff]
      exact hz
    · apply t.centerMass_mem_convexHull hw₀
      · simp only [hw₁, zero_lt_one]
      · exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)
  · exact iUnion_subset fun i => iUnion_subset convexHull_mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
refine_1 :
  Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
have refine_2 : Subset.{u_3} (α := Set E)
  (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
  ((convexHull R : (a : Set E) → Set E) s)
Tactic: classical
  refine Subset.antisymm ?_ ?_
  · rw [_root_.convexHull_eq]
    rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    simp only [mem_iUnion]
    refine ⟨t.image z, ?_, ?_⟩
    · rw [coe_image, Set.image_subset_iff]
      exact hz
    · apply t.centerMass_mem_convexHull hw₀
      · simp only [hw₁, zero_lt_one]
      · exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)
  · exact iUnion_subset fun i => iUnion_subset convexHull_mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
p₁ p₂ : E
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))
have rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
Tactic: rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
p₁ p₂ : E
rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))
have rw₁ : Eq (α := Submodule R E)
  (AffineSubspace.direction (P := E) (affineSpan R ((convexHull R : (a : Set E) → Set E) {p₁, p₂}))) (R ∙ (p₂ -ᵥ p₁))
Tactic: rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
p₁ p₂ : E
rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₁ :
  Eq (α := Submodule R E)
    (AffineSubspace.direction (P := E) (affineSpan R ((convexHull R : (a : Set E) → Set E) {p₁, p₂}))) (R ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))
have rw₂ : Eq (α := Submodule R E) (AffineSubspace.direction (P := E) (affineSpan R {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
Tactic: rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
p₁ p₂ : E
rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₁ :
  Eq (α := Submodule R E)
    (AffineSubspace.direction (P := E) (affineSpan R ((convexHull R : (a : Set E) → Set E) {p₁, p₂}))) (R ∙ (p₂ -ᵥ p₁))
rw₂ : Eq (α := Submodule R E) (AffineSubspace.direction (P := E) (affineSpan R {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))
have rw₃ : Eq (α := Submodule R E) (vectorSpan R (P := E) {p₁, p₂}) (R ∙ (p₂ -ᵥ p₁))
Tactic: rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
p₁ p₂ : E
rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₁ :
  Eq (α := Submodule R E)
    (AffineSubspace.direction (P := E) (affineSpan R ((convexHull R : (a : Set E) → Set E) {p₁, p₂}))) (R ∙ (p₂ -ᵥ p₁))
rw₂ : Eq (α := Submodule R E) (AffineSubspace.direction (P := E) (affineSpan R {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₃ : Eq (α := Submodule R E) (vectorSpan R (P := E) {p₁, p₂}) (R ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))
have rw₄ : Eq (α := Submodule R E) (R ∙ (p₂ -ᵥ p₁)) (R ∙ (p₂ -ᵥ p₁))
Tactic: rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
p₁ p₂ : E
rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₁ :
  Eq (α := Submodule R E)
    (AffineSubspace.direction (P := E) (affineSpan R ((convexHull R : (a : Set E) → Set E) {p₁, p₂}))) (R ∙ (p₂ -ᵥ p₁))
rw₂ : Eq (α := Submodule R E) (AffineSubspace.direction (P := E) (affineSpan R {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₃ : Eq (α := Submodule R E) (vectorSpan R (P := E) {p₁, p₂}) (R ∙ (p₂ -ᵥ p₁))
rw₄ : Eq (α := Submodule R E) (R ∙ (p₂ -ᵥ p₁)) (R ∙ (p₂ -ᵥ p₁))
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))
have rw₅ : Eq (α := Submodule R E) (R ∙ (p₂ - p₁)) (R ∙ (p₂ - p₁))
Tactic: rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
hx : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set F) ((convexHull R : (a : Set F) → Set F) t : Set F) y
⊢ Membership.mem (γ := Set (E × F)) ((convexHull R : (a : Set (E × F)) → Set (E × F)) (s ×ˢ t) : Set (E × F)) (x, y)
have rw : ∀
  (hx :
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x)
  (hy :
    ∃ (ι : Type) (x : Fintype ι) (w : ι → R) (z : ι → F),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y),
  ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
Tactic: rw [mem_convexHull_iff_exists_fintype] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
hx :
  ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
    (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x
hy :
  ∃ (ι : Type) (x : Fintype ι) (w : ι → R) (z : ι → F),
    (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y
⊢ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
have obtain : ∀ (ι : Type) (w : Fintype ι) (w_1 : ι → R) (f : ι → E) (hw₀ : ∀ (i : ι), 0 ≤ w_1 i)
  (hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w_1 i) 1) (hfs : ∀ (i : ι), f i ∈ s) (hf : ∑ i : ι, w_1 i • f i = x),
  ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
hy :
  ∃ (ι : Type) (x : Fintype ι) (w : ι → R) (z : ι → F),
    (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
⊢ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
have obtain : ∀ (κ : Type) (w : Fintype κ) (v : κ → R) (g : κ → F) (hv₀ : ∀ (i : κ), 0 ≤ v i)
  (hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1) (hgt : ∀ (i : κ), g i ∈ t) (hg : ∑ i : κ, v i • g i = y),
  ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ 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
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
have rw : Eq.{u_1 + 1} (α := R) (∑ x : ι, ∑ y : κ, w (x, y).1 * v (x, y).2) 1
Tactic: rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
rw : Eq.{u_1 + 1} (α := R) (∑ x : ι, ∑ y : κ, w (x, y).1 * v (x, y).2) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
have rw₁ : HMul.hMul (α := R) (∑ i : ι, w i) (∑ j : κ, v j) = 1
Tactic: rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
rw : Eq.{u_1 + 1} (α := R) (∑ x : ι, ∑ y : κ, w (x, y).1 * v (x, y).2) 1
rw₁ : HMul.hMul (α := R) (∑ i : ι, w i) (∑ j : κ, v j) = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
have rw₂ : HMul.hMul (α := R) 1 (∑ j : κ, v j) = 1
Tactic: rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
rw : Eq.{u_1 + 1} (α := R) (∑ x : ι, ∑ y : κ, w (x, y).1 * v (x, y).2) 1
rw₁ : HMul.hMul (α := R) (∑ i : ι, w i) (∑ j : κ, v j) = 1
rw₂ : HMul.hMul (α := R) 1 (∑ j : κ, v j) = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
have rw₃ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
rw : Eq.{u_1 + 1} (α := R) (∑ x : ι, ∑ y : κ, w (x, y).1 * v (x, y).2) 1
rw₁ : HMul.hMul (α := R) (∑ i : ι, w i) (∑ j : κ, v j) = 1
rw₂ : HMul.hMul (α := R) 1 (∑ j : κ, v j) = 1
rw₃ : HMul.hMul (α := R) 1 1 = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
have rw₄ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
⊢ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
have h_sum : Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
⊢ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
have refine : ∑ i : ι × κ,
    HSMul.hSMul (α := R) (β := E × F) ((fun (p : ι × κ) ↦ w p.1 * v p.2) i) ((fun (p : ι × κ) ↦ (f p.1, g p.2)) 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 _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
ι : Type
w_1 : Fintype ι
w : ι → R
f : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hfs : ∀ (i : ι), f i ∈ s
hf : ∑ i : ι, w i • f i = x
κ : Type
w_2 : Fintype κ
v : κ → R
g : κ → F
hv₀ : ∀ (i : κ), 0 ≤ v i
hv₁ : Eq.{u_1 + 1} (α := R) (∑ i : κ, v i) 1
hgt : ∀ (i : κ), g i ∈ t
hg : ∑ i : κ, v i • g i = y
h_sum : Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1
⊢ ∑ i : ι × κ,
      HSMul.hSMul (α := R) (β := E × F) ((fun (p : ι × κ) ↦ w p.1 * v p.2) i) ((fun (p : ι × κ) ↦ (f p.1, g p.2)) i) =
    (x, y)
have fst : (∑ i : ι × κ,
      HSMul.hSMul (α := R) (β := E × F) ((fun (p : ι × κ) ↦ w p.1 * v p.2) i)
        ((fun (p : ι × κ) ↦ (f p.1, g p.2)) i)).1 =
  (x, y).1
Tactic: ext