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
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
⊢ ∑ 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 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
Tactic: ext
-- 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)).1 =
    (x, y).1
have fst : (∑ x : ι × κ, (w x.1 * v x.2) • (f x.1, g x.2)).1 = x
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]
-- 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
fst fst₁ : (∑ x : ι × κ, (w x.1 * v x.2) • (f x.1, g x.2)).1 = 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
have fst₂ : ∑ c : ι × κ, ((w c.1 * v c.2) • (f c.1, g c.2)).1 = x
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]
-- 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
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
⊢ (∑ 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
have fst₃ : ∑ x : ι × κ, (w x.1 * v x.2) • f x.1 = x
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]
-- 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
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
⊢ (∑ 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
have fst₄ : ∑ x : ι, ∑ x_1 : κ, (w x * v x_1) • f x = x
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]
-- 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
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
⊢ (∑ 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
have fst₅ : ∑ x : ι, ∑ x_1 : κ, (v x_1 * w x) • f x = x
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]
-- 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
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
⊢ (∑ 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
have fst₆ : ∑ x : ι, ∑ x_1 : κ, v x_1 • w x • f x = x
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]
-- 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
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
⊢ (∑ 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
have fst₇ : ∑ y : κ, ∑ x : ι, v y • w x • f x = x
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]
-- 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
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
⊢ (∑ 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
have fst₈ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i : κ, v i) (∑ j : ι, w j • f j) = x
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]
-- 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
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
⊢ (∑ 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
have fst₉ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) 1 (∑ j : ι, w j • f j) = x
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]
-- 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)).2 =
    (x, y).2
have snd : (∑ x : ι × κ, (w x.1 * v x.2) • (f x.1, g x.2)).2 = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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
snd snd₁ : (∑ x : ι × κ, (w x.1 * v x.2) • (f x.1, g x.2)).2 = 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
have snd₂ : ∑ c : ι × κ, ((w c.1 * v c.2) • (f c.1, g c.2)).2 = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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
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
⊢ (∑ 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
have snd₃ : ∑ x : ι × κ, (w x.1 * v x.2) • g x.2 = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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
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
⊢ (∑ 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
have snd₄ : ∑ x : ι, ∑ x_1 : κ, (w x * v x_1) • g x_1 = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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
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
⊢ (∑ 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
have snd₅ : ∑ x : ι, ∑ x_1 : κ, w x • v x_1 • g x_1 = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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
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
⊢ (∑ 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
have snd₆ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := F) (∑ i : ι, w i) (∑ j : κ, v j • g j) = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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
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
⊢ (∑ 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
have snd₇ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := F) 1 (∑ j : κ, v j • g j) = y
Tactic: simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum,
      hw₁, one_smul, hg]
-- 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 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)
have 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)
Tactic: simp_rw [← add_image_prod, ← IsLinearMap.isLinearMap_add.image_convexHull, convexHull_prod]
-- 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 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)
⊢ (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)
have 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))
Tactic: simp_rw [← add_image_prod, ← IsLinearMap.isLinearMap_add.image_convexHull, convexHull_prod]
-- 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 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)
have 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)
Tactic: simp_rw [sub_eq_add_neg, convexHull_add, ← convexHull_neg]