awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Combination
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
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)
⊢ ∃ (ι : 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
-- Module: Mathlib.Analysis.Convex.Combination
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
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)
⊢ ∃ (ι : 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
-- Module: Mathlib.Analysis.Convex.Combination
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
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i : ι × κ, w i.1 * v i.2) 1

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

Premises used: mul_one, Fintype.sum_prod_type, Finset.sum_mul_sum
-- Module: Mathlib.Analysis.Convex.Combination
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

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]
-- Module: Mathlib.Analysis.Convex.Combination
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)

Tactic:
⟨ι × κ, 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 _⟩, ?_⟩

Premises used: mul_nonneg, HMul.hMul, inferInstance, Prod.mk, Prod.fst, And.intro, Exists.intro, Prod, Prod.snd
-- Module: Mathlib.Analysis.Convex.Combination
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
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)
⊢ ∃ (ι : 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:
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 _⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Combination
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
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
snd :
  (∑ i : ι × κ,
        HSMul.hSMul (α := R) (β := E × F) ((fun (p : ι × κ) ↦ w p.1 * v p.2) i)
          ((fun (p : ι × κ) ↦ (f p.1, g p.2)) i)).2 =
    (x, y).2
⊢ ∑ 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:
ext
-- Module: Mathlib.Analysis.Convex.Combination
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
fst fst₁ : (∑ x : ι × κ, (w x.1 * v x.2) • (f x.1, g x.2)).1 = x
fst₂ : ∑ c : ι × κ, ((w c.1 * v c.2) • (f c.1, g c.2)).1 = x
fst₃ : ∑ x : ι × κ, (w x.1 * v x.2) • f x.1 = x
fst₄ : ∑ x : ι, ∑ x_1 : κ, (w x * v x_1) • f x = x
fst₅ : ∑ x : ι, ∑ x_1 : κ, (v x_1 * w x) • f x = x
fst₆ : ∑ x : ι, ∑ x_1 : κ, v x_1 • w x • f x = x
fst₇ : ∑ y : κ, ∑ x : ι, v y • w x • f x = x
fst₈ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i : κ, v i) (∑ j : ι, w j • f j) = x
fst₉ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) 1 (∑ j : ι, w j • f j) = x
fst₁₀ : ∑ j : ι, w j • f j = x
⊢ (∑ 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:
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]

Premises used: one_smul, Fintype.sum_smul_sum, mul_comm, Prod.fst_sum, Prod.smul_mk, Finset.sum_comm, Fintype.sum_prod_type, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
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
snd snd₁ : (∑ x : ι × κ, (w x.1 * v x.2) • (f x.1, g x.2)).2 = y
snd₂ : ∑ c : ι × κ, ((w c.1 * v c.2) • (f c.1, g c.2)).2 = y
snd₃ : ∑ x : ι × κ, (w x.1 * v x.2) • g x.2 = y
snd₄ : ∑ x : ι, ∑ x_1 : κ, (w x * v x_1) • g x_1 = y
snd₅ : ∑ x : ι, ∑ x_1 : κ, w x • v x_1 • g x_1 = y
snd₆ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := F) (∑ i : ι, w i) (∑ j : κ, v j • g j) = y
snd₇ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := F) 1 (∑ j : κ, v j • g j) = y
snd₈ : ∑ j : κ, v j • g j = y
⊢ (∑ i : ι × κ,
        HSMul.hSMul (α := R) (β := E × F) ((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]

Premises used: Prod.snd_sum, one_smul, Fintype.sum_smul_sum, Prod.smul_mk, Fintype.sum_prod_type, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
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
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
s : Set E
t : Set F
⊢ (convexHull R : (a : Set (E × F)) → Set (E × F)) (s ×ˢ t) =
    SProd.sprod (α := Set E) (β := Set F) ((convexHull R : (a : Set E) → Set E) s : Set E)
      ((convexHull R : (a : Set F) → Set F) t : Set F)

Tactic:
Subset.antisymm
      (convexHull_min (prod_mono (subset_convexHull _ _) <| subset_convexHull _ _) <|
        (convex_convexHull _ _).prod <| convex_convexHull _ _) <|
    prod_subset_iff.2 fun _ hx _ => mk_mem_convexHull_prod hx

Premises used: Set.Subset.antisymm, Iff.mpr, subset_convexHull, Set.prod_subset_iff, mk_mem_convexHull_prod, convex_convexHull, Convex.prod, convexHull_min, Set.prod_mono
-- Module: Mathlib.Analysis.Convex.Combination
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 t : Set E
simp_rw :
  Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t) : Set E)
    ((fun (x : E × E) ↦ x.1 + x.2) ''
        SProd.sprod (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
          ((convexHull R : (a : Set E) → Set E) t : Set E) :
      Set E)
simp_rw₁ :
  Eq (α := Set E) ((fun (x : E × E) ↦ x.1 + x.2) '' (convexHull R : (a : Set (E × E)) → Set (E × E)) (s ×ˢ t))
    ((fun (x : E × E) ↦ x.1 + x.2) ''
      SProd.sprod (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
        ((convexHull R : (a : Set E) → Set E) t : Set E))
⊢ (convexHull R : (a : Set E) → Set E) (s + t) =
    HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      ((convexHull R : (a : Set E) → Set E) t : Set E)

Tactic:
simp_rw [← add_image_prod, ← IsLinearMap.isLinearMap_add.image_convexHull, convexHull_prod]

Premises used: IsLinearMap.image_convexHull, Set.add_image_prod, IsLinearMap.isLinearMap_add, convexHull_prod
-- Module: Mathlib.Analysis.Convex.Combination
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 t : Set E
simp_rw :
  (convexHull R : (a : Set E) → Set E) (s + -t) =
    HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      (-(convexHull R : (a : Set E) → Set E) t : Set E)
simp_rw₁ :
  HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      ((convexHull R : (a : Set E) → Set E) (-t) : Set E) =
    HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      (-(convexHull R : (a : Set E) → Set E) t : Set E)
⊢ (convexHull R : (a : Set E) → Set E) (s - t) =
    HSub.hSub (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      ((convexHull R : (a : Set E) → Set E) t : Set E)

Tactic:
simp_rw [sub_eq_add_neg, convexHull_add, ← convexHull_neg]

Premises used: convexHull_add, sub_eq_add_neg, convexHull_neg
-- Module: Mathlib.Analysis.Convex.Combination
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
l : List (Set E)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) l.sum : Set E)
    (List.sum (List.map (⇑(convexHull R) : (a : Set E) → Set E) l) : Set E)

Tactic:
map_list_sum (convexHullAddMonoidHom R E) l

Premises used: map_list_sum, convexHullAddMonoidHom
-- Module: Mathlib.Analysis.Convex.Combination
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 : Multiset (Set E)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s.sum : Set E)
    (Multiset.sum (Multiset.map (⇑(convexHull R) : (a : Set E) → Set E) s) : Set E)

Tactic:
map_multiset_sum (convexHullAddMonoidHom R E) s

Premises used: map_multiset_sum, convexHullAddMonoidHom
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
s : Finset ι
t : ι → Set E
⊢ Eq.{u_3 + 1} (α := Set E) ((convexHull R : (a : Set E) → Set E) (∑ i ∈ s, t i) : Set E)
    (∑ i ∈ s, (convexHull R : (a : Set E) → Set E) (t i) : Set E)

Tactic:
map_sum (convexHullAddMonoidHom R E) _ _

Premises used: map_sum, convexHullAddMonoidHom
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
rw :
  Eq.{u_3 + 1} (α := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
⊢ Eq.{u_3 + 1} (α := Set E)
    ((convexHull R : (a : Set E) → Set E) (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    ({x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} : Set E)

Tactic:
rw [convexHull_range_eq_exists_affineCombination]

Premises used: convexHull_range_eq_exists_affineCombination
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
h :
  ∀ (x : E),
    Membership.mem (γ := Set E)
        {x : E |
          ∃ (s : Finset ι) (w : ι → R),
            (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
        x ↔
      Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Eq.{u_3 + 1} (α := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
x : E
⊢ Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x

Tactic:
⟨?_, fun hx => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
x : E
h :
  Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x →
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
h₁ :
  ∀
    (hx :
      Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
        x),
    Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x
⊢ Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x

Tactic:
refine ⟨?_, fun hx => ?_⟩
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
pos :
  ∀ (hi : i ∈ s),
    LE.le.{u_1} (α := R) (0 : R)
      ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
neg :
  ∀ (hi : i ∉ s),
    LE.le.{u_1} (α := R) (0 : R)
      ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
pos : 0 ≤ w i
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)

Tactic:
rw [b.coord_apply_combination_of_mem hi hw₁]

Premises used: AffineBasis.coord_apply_combination_of_mem
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ w i

Tactic:
hw₀ i hi
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ w i

Tactic:
exact hw₀ i hi
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∉ s
neg neg₁ : LE.le.{u_1} (α := R) 0 0
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)

Tactic:
rw [b.coord_apply_combination_of_notMem hi hw₁]

Premises used: AffineBasis.coord_apply_combination_of_notMem
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
rw : Membership.mem (γ := AffineSubspace R E) ⊤ x
⊢ Membership.mem (γ := AffineSubspace R E) (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E))) x

Tactic:
rw [b.tot]

Premises used: AffineBasis.tot
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Membership.mem (γ := AffineSubspace R E) ⊤ x

Tactic:
AffineSubspace.mem_top R E x

Premises used: AffineSubspace.mem_top
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Membership.mem (γ := AffineSubspace R E) ⊤ x

Tactic:
exact AffineSubspace.mem_top R E x

Premises used: AffineSubspace.mem_top
-- Module: Mathlib.Analysis.Convex.Combination
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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Membership.mem (γ := AffineSubspace R E) (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E))) x

Tactic:
have hx' : x ∈ affineSpan R (range b) := by
      rw [b.tot]
      exact AffineSubspace.mem_top R E x