awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
have inl : ∀ (hxy : x ≤ y), a • x + b • y ∈ s
Tactic: obtain hxy | hyx := h _ hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (hxy : x ≤ y), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s
have inr : ∀ (hyx : y ≤ x), a • x + b • y ∈ s
Tactic: obtain hxy | hyx := h _ hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ∈ s
have inl : x ≤ a • x + b • y
Tactic: refine hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
inl : x ≤ a • x + b • y
⊢ a • x + b • y ∈ s
have inl₁ : a • x + b • y ≤ y
Tactic: refine hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ x ≤ a • x + b • y
have x₁ : a • x + b • x ≤ a • x + b • y
Tactic: calc
        x = a • x + b • x := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ a • x + b • y ≤ y
have a₁ : a • x + b • y ≤ a • y + b • y
Tactic: calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ∈ s
have inr : y ≤ a • x + b • y
Tactic: refine hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
inr : y ≤ a • x + b • y
⊢ a • x + b • y ∈ s
have inr₁ : a • x + b • y ≤ x
Tactic: refine hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ y ≤ a • x + b • y
have y₁ : a • y + b • y ≤ a • x + b • y
Tactic: calc
        y = a • y + b • y := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hyx : y ≤ x
⊢ a • x + b • y ≤ x
have a₁ : a • x + b • y ≤ a • x + b • x
Tactic: calc
      a • x + b • y ≤ a • x + b • x := by gcongr
      _ = x := Convex.combo_self hab _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ s.OrdConnected
have simp_rw : StarConvex 𝕜 x s ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s
Tactic: simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
simp_rw : StarConvex 𝕜 x s ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s
⊢ StarConvex 𝕜 x s ↔ s.OrdConnected
have simp_rw₁ : (∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s
Tactic: simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
⊢ stdSimplex 𝕜 ι = (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1}
have h : ∀ (f : ι → 𝕜),
  f ∈ stdSimplex 𝕜 ι ↔
    Membership.mem (γ := Set (ι → 𝕜))
      ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1}) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)
have refine_1 : ∀ (f : ι → 𝕜) (hf : f ∈ stdSimplex 𝕜 ι) (g : ι → 𝕜) (hg : g ∈ stdSimplex 𝕜 ι) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hab : a + b = 1) (x : ι), 0 ≤ (a • f + b • g) x
Tactic: refine fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
refine_1 :
  ∀ (f : ι → 𝕜) (hf : f ∈ stdSimplex 𝕜 ι) (g : ι → 𝕜) (hg : g ∈ stdSimplex 𝕜 ι) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hab : a + b = 1) (x : ι), 0 ≤ (a • f + b • g) x
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)
have refine_2 : ∀ (f : ι → 𝕜) (hf : f ∈ stdSimplex 𝕜 ι) (g : ι → 𝕜) (hg : g ∈ stdSimplex 𝕜 ι) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hab : a + b = 1), Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f + b • g) x) 1
Tactic: refine fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f + b • g) x) 1
have refine_2 : Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
Tactic: simp_rw [Pi.add_apply, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₂ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
refine_2₂ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₃ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
refine_2₂ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₃ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₄ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
refine_2₂ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₃ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₄ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₅ : a * 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
refine_2₂ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₃ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₄ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
refine_2₅ : a * 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₆ : a * 1 + b * 1 = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : HAdd.hAdd (α := 𝕜) (∑ x : ι, a • f x) (∑ x : ι, b • g x) = 1
refine_2₁ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + ∑ x : ι, b • g x = 1
refine_2₂ : HSMul.hSMul (β := 𝕜) a (∑ x : ι, f x) + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₃ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b (∑ x : ι, g x) = 1
refine_2₄ : HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
refine_2₅ : a * 1 + HSMul.hSMul (β := 𝕜) b 1 = 1
refine_2₆ : a * 1 + b * 1 = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
have refine_2₇ : a + b * 1 = 1
Tactic: rwa [Finset.sum_add_distrib, ← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
      smul_eq_mul, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Nonempty ι
inst_5 : Subsingleton ι
⊢ stdSimplex 𝕜 ι = {fun (x : ι) ↦ 1}
have intro : ∀ (val : Unique ι), stdSimplex 𝕜 ι = {fun (x : ι) ↦ 1}
Tactic: cases nonempty_unique ι
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Nonempty ι
inst_5 : Subsingleton ι
val : Unique ι
⊢ stdSimplex 𝕜 ι = {fun (x : ι) ↦ 1}
have intro : ∀ x ∈ stdSimplex 𝕜 ι, x = fun (x : ι) ↦ 1
Tactic: refine eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Nonempty ι
inst_5 : Subsingleton ι
val : Unique ι
f : ι → 𝕜
hf : Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1
⊢ f = fun (x : ι) ↦ 1
have hf₁ : f default = 1
Tactic: rw [Fintype.sum_unique] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
h : f ∈ stdSimplex 𝕜 ι
⊢ Membership.mem (γ := Set (ι → 𝕜)) (Icc 0 1) f
have rw : ∀ (i : ι), Membership.mem (γ := Set (ι → 𝕜)) (Function.eval (β := fun (i : ι) ↦ 𝕜) i ⁻¹' Icc (0 i) (1 i)) f
Tactic: rw [← pi_univ_Icc, univ_pi_eq_iInter, mem_iInter]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : ZeroLEOneClass 𝕜
inst_3 : IsOrderedRing 𝕜
⊢ Eq (α := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2))
    [Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1 -[𝕜] Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1]
have refine : Subset (α := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2))
  [Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1 -[𝕜] Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1]
Tactic: refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
Goal:
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : ZeroLEOneClass 𝕜
inst_3 : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : Eq.{u_2 + 1} (α := 𝕜) (∑ x : Fin 2, f x) 1
⊢ Membership.mem (γ := Set (Fin 2 → 𝕜))
    [Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1 -[𝕜] Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1] f
have hf₂ : f 0 + f 1 = 1
Tactic: rw [Fin.sum_univ_two] at hf₁
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : ZeroLEOneClass 𝕜
inst_3 : IsOrderedRing 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ Membership.mem (γ := Set (Fin 2 → 𝕜))
    [Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1 -[𝕜] Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1] f
have refine : (HSMul.hSMul (β := Fin 2 → 𝕜) (f 0) (Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1) +
        HSMul.hSMul (β := Fin 2 → 𝕜) (f 1) (Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1))
      0 =
    f 0 ∧
  (HSMul.hSMul (β := Fin 2 → 𝕜) (f 0) (Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1) +
        HSMul.hSMul (β := Fin 2 → 𝕜) (f 1) (Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1))
      1 =
    f 1
Tactic: refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
⊢ (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) =
    stdSimplex R ι
have refine_1 : (range fun (i j : ι) ↦ if i = j then 1 else 0) ⊆ stdSimplex R ι
Tactic: refine Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
refine_1 : (range fun (i j : ι) ↦ if i = j then 1 else 0) ⊆ stdSimplex R ι
⊢ (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) =
    stdSimplex R ι
have refine_2 : stdSimplex R ι ⊆
  (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0)
Tactic: refine Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
w : (j : ι) → R
hw₀ : ∀ (x : ι), 0 ≤ w x
hw₁ : Eq.{u_1 + 1} (α := R) (∑ x : ι, w x) 1
⊢ Membership.mem (γ := Set ((j : ι) → R))
    ((convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) :
      Set ((j : ι) → R))
    w
have refine_2 : Membership.mem (γ := Set ((j : ι) → R))
  ((convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) :
    Set ((j : ι) → R))
  (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (w i) fun (j : ι) ↦ if i = j then 1 else 0)
Tactic: rw [pi_eq_sum_univ w]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
w : (j : ι) → R
hw₀ : ∀ (x : ι), 0 ≤ w x
hw₁ : Eq.{u_1 + 1} (α := R) (∑ x : ι, w x) 1
⊢ Membership.mem (γ := Set ((j : ι) → R))
    ((convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) :
      Set ((j : ι) → R))
    (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (w i) fun (j : ι) ↦ if i = j then 1 else 0)
have refine_2 : Membership.mem (γ := Set ((j : ι) → R))
  ((convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) :
    Set ((j : ι) → R))
  (Finset.centerMass Finset.univ w fun (i j : ι) ↦ if i = j then 1 else 0)
Tactic: rw [← Finset.univ.centerMass_eq_of_sum_1 _ hw₁]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
ι : Type u_2
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
⊢ (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R))
      (range fun (i : ι) ↦ Pi.single (M := fun (a : ι) ↦ R) i 1) =
    stdSimplex R ι
have h : ∀ (x x_1 : ι), Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : ι) ↦ R) x 1 x_1 : R) (if x = x_1 then 1 else 0 : R)
Tactic: convert! convexHull_basis_eq_stdSimplex R ι
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module R E
s : Set E
hs : s.Finite
this : Fintype (↑s : Type u_3) := hs.fintype (s := s)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (Set.image (α := (↑s : Type u_3) → R)
        (⇑(∑ x : (↑s : Type u_3),
              LinearMap.smulRight (S := R) (LinearMap.proj (φ := fun (i : (↑s : Type u_3)) ↦ R) x) (↑x : E)) :
          (a : (↑s : Type u_3) → R) → E)
        (stdSimplex R (↑s : Type u_3)) :
      Set E)
have rw : Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
  ((convexHull R : (a : Set E) → Set E)
      (range (ι := (↑s : Type u_3))
        (Function.comp (β := (↑s : Type u_3) → R)
          (⇑(∑ x : (↑s : Type u_3),
                LinearMap.smulRight (S := R) (LinearMap.proj (φ := fun (i : (↑s : Type u_3)) ↦ R) x) (↑x : E)) :
            (a : (↑s : Type u_3) → R) → E)
          fun (i j : (↑s : Type u_3)) ↦ if i = j then 1 else 0)) :
    Set E)
Tactic: rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
E : Type u_3
inst_3 : AddCommGroup E
inst_4 : Module R E
s : Set E
hs : s.Finite
this : Fintype (↑s : Type u_3) := hs.fintype (s := s)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    ((convexHull R : (a : Set E) → Set E)
        (range (ι := (↑s : Type u_3))
          (Function.comp (β := (↑s : Type u_3) → R)
            (⇑(∑ x : (↑s : Type u_3),
                  LinearMap.smulRight (S := R) (LinearMap.proj (φ := fun (i : (↑s : Type u_3)) ↦ R) x) (↑x : E)) :
              (a : (↑s : Type u_3) → R) → E)
            fun (i j : (↑s : Type u_3)) ↦ if i = j then 1 else 0)) :
      Set E)
have h : s =
  range (ι := (↑s : Type u_3))
    (Function.comp (β := (↑s : Type u_3) → R)
      (⇑(∑ x : (↑s : Type u_3),
            LinearMap.smulRight (S := R) (LinearMap.proj (φ := fun (i : (↑s : Type u_3)) ↦ R) x) (↑x : E)) :
        (a : (↑s : Type u_3) → R) → E)
      fun (i j : (↑s : Type u_3)) ↦ if i = j then 1 else 0)
Tactic: apply congr_arg