awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Star
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 • y + b • y

Tactic:
(Convex.combo_self hab _).symm

Premises used: Convex.combo_self, Eq.symm
-- Module: Mathlib.Analysis.Convex.Star
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
bc : 0 ≤ a
⊢ a • y + b • y ≤ a • x + b • y

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Star
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 • y + b • y ≤ a • x + b • y
⊢ y ≤ a • x + b • y

Tactic:
calc
        y = a • y + b • y := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr

Premises used: Convex.combo_self, Eq.symm
-- Module: Mathlib.Analysis.Convex.Star
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
bc : 0 ≤ b
⊢ a • x + b • y ≤ a • x + b • x

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Star
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 • x = x

Tactic:
Convex.combo_self hab _

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Star
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₁ : a • x + b • y ≤ a • x + b • x
⊢ a • x + b • y ≤ x

Tactic:
calc
      a • x + b • y ≤ a • x + b • x := by gcongr
      _ = x := Convex.combo_self hab _

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Star
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
simp_rw₁ : (∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s
⊢ StarConvex 𝕜 x s ↔ s.OrdConnected

Tactic:
simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]

Premises used: Set.ordConnected_iff_uIcc_subset_left, segment_eq_uIcc, starConvex_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
h :
  ∀ (f : ι → 𝕜),
    f ∈ stdSimplex 𝕜 ι ↔
      Membership.mem (γ := Set (ι → 𝕜))
        ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1}) f
⊢ stdSimplex 𝕜 ι = (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1}

Tactic:
ext f
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔
    Membership.mem (γ := Set (ι → 𝕜))
      ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1}) f

Tactic:
simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_setOf_eq]

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_iInter, stdSimplex
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedRing 𝕜
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)

Tactic:
fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩

Premises used: Set.Mem, setOf, stdSimplex, Convex, And.intro, StarConvex
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
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
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)

Tactic:
refine fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
x : ι
⊢ 0 ≤ (a • f + b • g) x

Tactic:
apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]

Premises used: mul_nonneg, add_nonneg, And.left
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 : Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f x + b • g x)) 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f + b • g) x) 1

Tactic:
simp_rw [Pi.add_apply, Pi.smul_apply]

Premises used: Pi.add_apply, Pi.smul_apply
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
refine_2₇ : a + b * 1 = 1
refine_2₈ refine_2₉ refine_2₁₀ refine_2₁₁ : a + b = 1
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, (a • f 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]

Premises used: Finset.sum_add_distrib, And.right, Finset.smul_sum, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : Subsingleton 𝕜
⊢ stdSimplex 𝕜 ι = univ

Tactic:
eq_univ_of_forall fun _ ↦ ⟨fun _ ↦ (Subsingleton.elim _ _).le, Subsingleton.elim _ _⟩

Premises used: Finset.univ, Eq.le, Set.eq_univ_of_forall, And.intro, Subsingleton.elim, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsEmpty ι
inst_4 : Nontrivial 𝕜
f : ι → 𝕜
hf : Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, f x) 1
⊢ False

Tactic:
simp at hf
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Nonempty ι
inst_5 : Subsingleton ι
intro : ∀ (val : Unique ι), stdSimplex 𝕜 ι = {fun (x : ι) ↦ 1}
⊢ stdSimplex 𝕜 ι = {fun (x : ι) ↦ 1}

Tactic:
cases nonempty_unique ι

Premises used: nonempty_unique
-- Module: Mathlib.Analysis.Convex.StdSimplex
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}

Tactic:
eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩

Premises used: Iff.mpr, Fintype.sum_unique, zero_le_one, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 ι
intro : ∀ x ∈ stdSimplex 𝕜 ι, x = fun (x : ι) ↦ 1
⊢ stdSimplex 𝕜 ι = {fun (x : ι) ↦ 1}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 default = 1

Tactic:
rw [Fintype.sum_unique] at hf

Premises used: Fintype.sum_unique
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 : f default = 1
⊢ f = fun (x : ι) ↦ 1

Tactic:
funext (Unique.forall_iff.2 hf)

Premises used: Iff.mpr, Unique.forall_iff, funext
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 : f default = 1
⊢ f = fun (x : ι) ↦ 1

Tactic:
exact funext (Unique.forall_iff.2 hf)

Premises used: Iff.mpr, Unique.forall_iff, funext
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
x : ι
⊢ Membership.mem (γ := Set 𝕜) (Icc 0 1) (f x)

Tactic:
⟨hf.1 x, hf.2 ▸ Finset.single_le_sum (fun y _ => hf.1 y) (Finset.mem_univ x)⟩

Premises used: Finset.mem_univ, Set.Mem, setOf, Eq.rec, Set.Icc, And.right, And.left, And.intro, Finset.single_le_sum
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
h : f ∈ stdSimplex 𝕜 ι
rw : ∀ (i : ι), Membership.mem (γ := Set (ι → 𝕜)) (Function.eval (β := fun (i : ι) ↦ 𝕜) i ⁻¹' Icc (0 i) (1 i)) f
⊢ Membership.mem (γ := Set (ι → 𝕜)) (Icc 0 1) f

Tactic:
rw [← pi_univ_Icc, univ_pi_eq_iInter, mem_iInter]

Premises used: Set.univ_pi_eq_iInter, Set.mem_iInter, Set.pi_univ_Icc
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : IsOrderedAddMonoid 𝕜
f : ι → 𝕜
h : f ∈ stdSimplex 𝕜 ι
⊢ ∀ (i : ι), Membership.mem (γ := Set (ι → 𝕜)) (Function.eval (β := fun (i : ι) ↦ 𝕜) i ⁻¹' Icc (0 i) (1 i)) f

Tactic:
simpa using fun i ↦ mem_Icc_of_mem_stdSimplex h i

Premises used: mem_Icc_of_mem_stdSimplex
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : ZeroLEOneClass 𝕜
i : ι
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑ x : ι, Pi.single (M := fun (j : ι) ↦ 𝕜) i 1 x) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : ZeroLEOneClass 𝕜
i : ι
⊢ (fun (x : ι) ↦ if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι

Tactic:
simpa only [@eq_comm _ i, ← Pi.single_apply] using single_mem_stdSimplex 𝕜 i

Premises used: Pi.single_apply, single_mem_stdSimplex, eq_comm
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
ι : Type u_1
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : ZeroLEOneClass 𝕜
inst_5 : IsOrderedRing 𝕜
i j : ι
⊢ [Pi.single (M := fun (a : ι) ↦ 𝕜) i 1 -[𝕜] Pi.single (M := fun (a : ι) ↦ 𝕜) j 1] ⊆ stdSimplex 𝕜 ι

Tactic:
(convex_stdSimplex 𝕜 ι).segment_subset (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

Premises used: single_mem_stdSimplex, convex_stdSimplex, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.StdSimplex
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]

Tactic:
Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)

Premises used: Set.Subset.antisymm, segment_single_subset_stdSimplex, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : ZeroLEOneClass 𝕜
inst_3 : IsOrderedRing 𝕜
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]
⊢ 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]

Tactic:
refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)

Premises used: Set.Subset.antisymm, segment_single_subset_stdSimplex, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
⊢ f 0 + f 1 = 1

Tactic:
rw [Fin.sum_univ_two] at hf₁

Premises used: Fin.sum_univ_two
-- Module: Mathlib.Analysis.Convex.StdSimplex
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

Tactic:
⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩

Premises used: Fin.forall_fin_two, Iff.mpr, Set.Mem, setOf, segment, funext, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
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
⊢ Membership.mem (γ := Set (Fin 2 → 𝕜))
    [Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 0 1 -[𝕜] Pi.single (M := fun (a : Fin 2) ↦ 𝕜) 1 1] f

Tactic:
refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
⊢ (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:
simp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
x : (↑(Icc 0 1) : Type u_1)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ x_1 : Fin 2, ![1 - (↑x : 𝕜), (↑x : 𝕜)] x_1) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type ?u.38335
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
f : (↑(stdSimplex 𝕜 (Fin 2)) : Type ?u.38335)
⊢ (↑f : Fin 2 → 𝕜) 0 + (↑f : Fin 2 → 𝕜) 1 = 1

Tactic:
simpa using f.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
f : (↑(stdSimplex 𝕜 (Fin 2)) : Type u_1)
⊢ (↑((fun (x : (↑(Icc 0 1) : Type u_1)) ↦
                (Subtype.mk (p := fun (x : Fin 2 → 𝕜) ↦ Membership.mem (γ := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2)) x)
                    ![1 - (↑x : 𝕜), (↑x : 𝕜)] ⋯ :
                  { x : Fin 2 → 𝕜 // Membership.mem (γ := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2)) x }))
              ((fun (f : (↑(stdSimplex 𝕜 (Fin 2)) : Type u_1)) ↦
                  (Subtype.mk (p := fun (x : 𝕜) ↦ Membership.mem (γ := Set 𝕜) (Icc 0 1) x) ((↑f : Fin 2 → 𝕜) 1) ⋯ :
                    { x : 𝕜 // Membership.mem (γ := Set 𝕜) (Icc 0 1) x }))
                f)) :
          Fin 2 → 𝕜)
        0 =
      (↑f : Fin 2 → 𝕜) 0 ∧
    (↑((fun (x : (↑(Icc 0 1) : Type u_1)) ↦
                (Subtype.mk (p := fun (x : Fin 2 → 𝕜) ↦ Membership.mem (γ := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2)) x)
                    ![1 - (↑x : 𝕜), (↑x : 𝕜)] ⋯ :
                  { x : Fin 2 → 𝕜 // Membership.mem (γ := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2)) x }))
              ((fun (f : (↑(stdSimplex 𝕜 (Fin 2)) : Type u_1)) ↦
                  (Subtype.mk (p := fun (x : 𝕜) ↦ Membership.mem (γ := Set 𝕜) (Icc 0 1) x) ((↑f : Fin 2 → 𝕜) 1) ⋯ :
                    { x : 𝕜 // Membership.mem (γ := Set 𝕜) (Icc 0 1) x }))
                f)) :
          Fin 2 → 𝕜)
        1 =
      (↑f : Fin 2 → 𝕜) 1

Tactic:
simp [← (show f.1 0 + f.1 1 = 1 by simpa using f.2.2)]
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
⊢ Eq (α := (↑(Icc 0 1) : Type u_1))
    ((stdSimplexEquivIcc 𝕜 : (a : (↑(stdSimplex 𝕜 (Fin 2)) : Type u_1)) → (↑(Icc 0 1) : Type u_1))
        (Subtype.mk (p := fun (x : Fin 2 → 𝕜) ↦ Membership.mem (γ := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2)) x)
          (Pi.single (M := fun (j : Fin 2) ↦ 𝕜) 0 1) ⋯) :
      (↑(Icc 0 1) : Type u_1))
    (0 : (↑(Icc 0 1) : Type u_1))

Tactic:
rfl

Premises used: Function.update, Set.Mem, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsOrderedRing 𝕜
⊢ Eq (α := (↑(Icc 0 1) : Type u_1))
    ((stdSimplexEquivIcc 𝕜 : (a : (↑(stdSimplex 𝕜 (Fin 2)) : Type u_1)) → (↑(Icc 0 1) : Type u_1))
        (Subtype.mk (p := fun (x : Fin 2 → 𝕜) ↦ Membership.mem (γ := Set (Fin 2 → 𝕜)) (stdSimplex 𝕜 (Fin 2)) x)
          (Pi.single (M := fun (j : Fin 2) ↦ 𝕜) 1 1) ⋯) :
      (↑(Icc 0 1) : Type u_1))
    (1 : (↑(Icc 0 1) : Type u_1))

Tactic:
rfl

Premises used: Function.update, Set.Mem, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 ι

Tactic:
Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_

Premises used: Set.Subset.antisymm, convex_stdSimplex, convexHull_min
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 ι
refine_2 :
  stdSimplex R ι ⊆
    (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0)
⊢ (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R)) (range fun (i j : ι) ↦ if i = j then 1 else 0) =
    stdSimplex R ι

Tactic:
refine Subset.antisymm (convexHull_min ?_ (convex_stdSimplex R ι)) ?_

Premises used: Set.Subset.antisymm, convex_stdSimplex, convexHull_min
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 ι
i : ι
⊢ (fun (i j : ι) ↦ (if i = j then 1 else 0 : R)) i ∈ stdSimplex R ι

Tactic:
ite_eq_mem_stdSimplex R i

Premises used: Set.Mem, ite_eq_mem_stdSimplex
-- Module: Mathlib.Analysis.Convex.StdSimplex
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 ι
i : ι
⊢ (fun (i j : ι) ↦ (if i = j then 1 else 0 : R)) i ∈ stdSimplex R ι

Tactic:
exact ite_eq_mem_stdSimplex R i

Premises used: ite_eq_mem_stdSimplex
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
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)
⊢ 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

Tactic:
rw [pi_eq_sum_univ w]

Premises used: pi_eq_sum_univ
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
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)
⊢ 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 [← Finset.univ.centerMass_eq_of_sum_1 _ hw₁]

Premises used: Finset.univ, Finset.centerMass_eq_of_sum_1
-- Module: Mathlib.Analysis.Convex.StdSimplex
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))
    (Finset.centerMass Finset.univ w fun (i j : ι) ↦ if i = j then 1 else 0)

Tactic:
Finset.univ.centerMass_mem_convexHull (fun i _ => hw₀ i) (hw₁.symm ▸ zero_lt_one)
      fun i _ => mem_range_self i

Premises used: Set.mem_range_self, Finset.univ, Set.Mem, Finset.centerMass_mem_convexHull