awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
⊢ Membership.mem (α := Y → S) (stdSimplex S Y) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s : Y → S)

Tactic:
⟨fun y ↦ ?_, ?_⟩

Premises used: Set.Mem, setOf, stdSimplex, And.intro
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
refine_1 : ∀ (y : Y), LE.le.{u_1} (α := S) (0 : S) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s y : S)
refine_2 : Eq.{u_1 + 1} (α := S) (∑ x : Y, (FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s x) 1
⊢ Membership.mem (α := Y → S) (stdSimplex S Y) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s : Y → S)

Tactic:
refine ⟨fun y ↦ ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
y : Y
refine_1 : 0 ≤ Finset.sum {x : X | f x = y} s
⊢ LE.le.{u_1} (α := S) (0 : S) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s y : S)

Tactic:
rw [FunOnFinite.linearMap_apply_apply]

Premises used: FunOnFinite.linearMap_apply_apply
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
y : Y
⊢ ∀ (i : X), Membership.mem (γ := Finset X) {x : X | f x = y} i → 0 ≤ s i

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
y : Y
⊢ 0 ≤ Finset.sum {x : X | f x = y} s

Tactic:
exact Finset.sum_nonneg (by aesop)

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
refine_2 : Eq.{u_1 + 1} (α := S) (∑ x : Y, Finset.sum {x_1 : X | f x_1 = x} s) (∑ x : X, s x)
⊢ Eq.{u_1 + 1} (α := S) (∑ x : Y, (FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s x) 1

Tactic:
simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]

Premises used: FunOnFinite.linearMap_apply_apply
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
⊢ Eq.{u_1 + 1} (α := S) (∑ x : Y, Finset.sum {x_1 : X | f x_1 = x} s) (∑ x : X, s x)

Tactic:
Finset.sum_fiberwise Finset.univ f s

Premises used: Finset.univ, Finset.sum_fiberwise
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1
⊢ Eq.{u_1 + 1} (α := S) (∑ x : Y, Finset.sum {x_1 : X | f x_1 = x} s) (∑ x : X, s x)

Tactic:
exact Finset.sum_fiberwise Finset.univ f s

Premises used: Finset.univ, Finset.sum_fiberwise
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
rintro :
  ∀ (s : X → S) (hs₀ : ∀ (x : X), 0 ≤ s x) (hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1),
    Membership.mem (α := Y → S) (stdSimplex S Y) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s : Y → S)
refine_1 :
  ∀ (s : X → S) (hs₀ : ∀ (x : X), 0 ≤ s x) (hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1) (y : Y),
    LE.le.{u_1} (α := S) (0 : S) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s y : S)
refine_2 refine_2₁ :
  ∀ (s : X → S) (hs₀ : ∀ (x : X), 0 ≤ s x) (hs₁ : Eq.{u_1 + 1} (α := S) (∑ x : X, s x) 1),
    Eq.{u_1 + 1} (α := S) (∑ x : Y, (FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s x) 1
⊢ (⇑(FunOnFinite.linearMap S S f) : (a : X → S) → Y → S) '' stdSimplex S X ⊆ stdSimplex S Y

Tactic:
classical
  rintro _ ⟨s, ⟨hs₀, hs₁⟩, rfl⟩
  refine ⟨fun y ↦ ?_, ?_⟩
  · rw [FunOnFinite.linearMap_apply_apply]
    exact Finset.sum_nonneg (by aesop)
  · simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]
    exact Finset.sum_fiberwise Finset.univ f s

Premises used: FunOnFinite.linearMap_apply_apply, Finset.sum_nonneg, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
f : X → Y
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
⊢ Membership.mem (α := Y → S) (γ := Set (Y → S))
    ((⇑(FunOnFinite.linearMap S S f) : (a : X → S) → Y → S) '' stdSimplex S X)
    ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) (⇑s : (a : X) → S) : Y → S)

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
f : X → Y
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
⊢ Eq (α := (a : Y) → S) (⇑(map f s) : (a : Y) → S)
    ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) (⇑s : (a : X) → S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
x : (↑(stdSimplex S X) : Type (max u_1 u_2))
⊢ map id x = x

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
f : X → Y
g : Y → Z
x : (↑(stdSimplex S X) : Type (max u_1 u_2))
h : ∀ (x_1 : Z), Eq.{u_1 + 1} (α := S) ((map g (map f x) : (a : Z) → S) x_1 : S) ((map (g ∘ f) x : (a : Z) → S) x_1 : S)
⊢ Eq (α := (↑(stdSimplex S Z) : Type (max u_1 u_4))) (map g (map f x)) (map (g ∘ f) x)

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
f : X → Y
g : Y → Z
x : (↑(stdSimplex S X) : Type (max u_1 u_2))
x_1 : Z
⊢ Eq.{u_1 + 1} (α := S) ((map g (map f x) : (a : Z) → S) x_1 : S) ((map (g ∘ f) x : (a : Z) → S) x_1 : S)

Tactic:
simp [FunOnFinite.linearMap_comp]

Premises used: FunOnFinite.linearMap_comp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : DecidableEq X
x : X
⊢ Eq (α := (a : X) → S) (⇑(vertex x) : (a : X) → S) (Pi.single (M := fun (j : X) ↦ S) x 1)

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
inst_5 : DecidableEq X
inst_6 : DecidableEq Y
f : X → Y
x : X
⊢ Eq (α := (↑(stdSimplex S Y) : Type (max u_1 u_3))) (map f (vertex x)) (vertex (f x))

Tactic:
aesop
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : IsOrderedRing S
inst_5 : TopologicalSpace S
inst_6 : IsTopologicalSemiring S
f : X → Y
⊢ Continuous (X := (↑(stdSimplex S X) : Type (max u_1 u_2))) (Y := (↑(stdSimplex S Y) : Type (max u_1 u_3))) (map f)

Tactic:
Continuous.subtype_mk ((FunOnFinite.continuous_linearMap S S f).comp continuous_induced_dom) _

Premises used: stdSimplex.map, Continuous.comp, FunOnFinite.continuous_linearMap, Continuous.subtype_mk, continuous_induced_dom
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : Nontrivial S
inst_5 : DecidableEq X
x y : X
h : Eq (α := (↑(stdSimplex S X) : Type (max u_1 u_2))) (vertex x) (vertex y)
⊢ Eq.{u_1 + 1} (α := S) ((vertex x : (a : X) → S) x : S) ((vertex y : (a : X) → S) x : S)

Tactic:
replace h := DFunLike.congr_fun h x
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : Nontrivial S
inst_5 : DecidableEq X
x y : X
h : Eq.{u_1 + 1} (α := S) ((vertex x : (a : X) → S) x : S) ((vertex y : (a : X) → S) x : S)
by_contra! : ∀ (this : x ≠ y), False
⊢ x = y

Tactic:
by_contra!
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : Nontrivial S
inst_5 : DecidableEq X
x y : X
h : Eq.{u_1 + 1} (α := S) ((vertex x : (a : X) → S) x : S) ((vertex y : (a : X) → S) x : S)
this : x ≠ y
⊢ False

Tactic:
simp [Pi.single_eq_of_ne this] at h

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nonempty X
⊢ Nonempty (↑(stdSimplex S X) : Type (max u_1 u_2))

Tactic:
⟨vertex (Classical.arbitrary _)⟩

Premises used: Nonempty.intro, stdSimplex.vertex, Classical.arbitrary
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nonempty X
⊢ Nonempty (↑(stdSimplex S X) : Type (max u_1 u_2))

Tactic:
exact ⟨vertex (Classical.arbitrary _)⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nonempty X
⊢ Nonempty (↑(stdSimplex S X) : Type (max u_1 u_2))

Tactic:
classical
  exact ⟨vertex (Classical.arbitrary _)⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
inst_7 : Nontrivial X
obtain :
  ∀ (x y : X) (hxy : x ≠ y),
    ∃ (x : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y
⊢ ∃ (x : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y

Tactic:
obtain ⟨x, y, hxy⟩ := exists_pair_ne X

Premises used: exists_pair_ne
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
inst_7 : Nontrivial X
x y : X
hxy : x ≠ y
⊢ ∃ (x : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y

Tactic:
⟨vertex x, vertex y, fun h ↦ hxy (vertex_injective h)⟩

Premises used: stdSimplex.vertex, stdSimplex.vertex_injective, Exists.intro
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
inst_7 : Nontrivial X
x y : X
hxy : x ≠ y
⊢ ∃ (x : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y

Tactic:
exact ⟨vertex x, vertex y, fun h ↦ hxy (vertex_injective h)⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Nontrivial S
inst_7 : Nontrivial X
obtain :
  ∀ (x y : X) (hxy : x ≠ y),
    ∃ (x : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y
⊢ ∃ (x : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y

Tactic:
classical
    obtain ⟨x, y, hxy⟩ := exists_pair_ne X
    exact ⟨vertex x, vertex y, fun h ↦ hxy (vertex_injective h)⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
h : ∀ (i : X), Eq.{u_1 + 1} (α := S) ((s : (a : X) → S) i : S) ((t : (a : X) → S) i : S)
⊢ s = t

Tactic:
ext i
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
u : (↑(stdSimplex S X) : Type (max u_1 u_2))
⊢ i ∉ Finset.univ → Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) i : S) (0 : S)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
u : (↑(stdSimplex S X) : Type (max u_1 u_2))
rw :
  ∀ (b : X),
    Membership.mem (γ := Finset X) Finset.univ b → b ≠ i → Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) b : S) (0 : S)
⊢ Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) i : S) (1 : S)

Tactic:
rw [← sum_eq_one u, Finset.sum_eq_single i _ (by simp)]

Premises used: Finset.sum_eq_single, stdSimplex.sum_eq_one
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
u : (↑(stdSimplex S X) : Type (max u_1 u_2))
j : X
_ : Membership.mem (γ := Finset X) Finset.univ j → j ≠ i → Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) j : S) (0 : S)
⊢ Membership.mem (γ := Finset X) Finset.univ j → j ≠ i → Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) j : S) (0 : S)

Tactic:
_
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
u : (↑(stdSimplex S X) : Type (max u_1 u_2))
j : X
h : Membership.mem (γ := Finset X) Finset.univ j
hj : j ≠ i
⊢ Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) j : S) (0 : S)

Tactic:
(hj (Subsingleton.elim j i)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
u : (↑(stdSimplex S X) : Type (max u_1 u_2))
j : X
h : Membership.mem (γ := Finset X) Finset.univ j
hj : j ≠ i
⊢ Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) j : S) (0 : S)

Tactic:
exact (hj (Subsingleton.elim j i)).elim

Premises used: False.elim, Subsingleton.elim
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
⊢ ∀ (u : (↑(stdSimplex S X) : Type (max u_1 u_2))), Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) i : S) (1 : S)

Tactic:
have (u : stdSimplex S X) : u i = 1 := by
      rw [← sum_eq_one u, Finset.sum_eq_single i _ (by simp)]
      intro j _ hj
      exact (hj (Subsingleton.elim j i)).elim
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Subsingleton X
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
i : X
this : ∀ (u : (↑(stdSimplex S X) : Type (max u_1 u_2))), Eq.{u_1 + 1} (α := S) ((u : (a : X) → S) i : S) (1 : S)
⊢ Eq.{u_1 + 1} (α := S) ((s : (a : X) → S) i : S) ((t : (a : X) → S) i : S)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Unique X
⊢ ∀ (x : X), LE.le.{u_1} (α := S) 0 (1 x)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Unique X
⊢ Eq.{u_1 + 1} (α := S) (∑ x : X, 1 x) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
inst_5 : IsOrderedRing S
inst_6 : Unique X
⊢ ∀ (a : (↑(stdSimplex S X) : Type (max u_1 u_2))), a = Subtype.mk (p := fun (x : X → S) ↦ x ∈ stdSimplex S X) 1 ⋯

Tactic:
subsingleton
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : Unique X
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
⊢ s = default

Tactic:
subsingleton
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : Unique X
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
obtain : Eq.{u_1 + 1} (α := S) ((default : (a : X) → S) x : S) (1 : S)
⊢ Eq.{u_1 + 1} (α := S) ((s : (a : X) → S) x : S) (1 : S)

Tactic:
obtain rfl : s = default := by subsingleton

Premises used: Inhabited.default, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
inst_2 : Fintype X
inst_3 : IsOrderedRing S
inst_4 : Unique X
x : X
⊢ Eq.{u_1 + 1} (α := S) ((default : (a : X) → S) x : S) (1 : S)

Tactic:
rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst_2 : Fintype X
inst_3 : Fintype Y
inst_4 : Fintype Z
𝕜 : Type u_5
inst_5 : Field 𝕜
inst_6 : LinearOrder 𝕜
inst_7 : IsStrictOrderedRing 𝕜
inst_8 : Nonempty X
⊢ (fun (i : X) ↦ (↑(Fintype.card X) : 𝕜)⁻¹) ∈ stdSimplex 𝕜 X

Tactic:
simp [stdSimplex]

Premises used: stdSimplex
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
X : Type u_2
inst : Fintype X
𝕜 : Type u_5
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : Nonempty X
x : X
⊢ Eq.{u_5 + 1} (α := 𝕜) ((↑barycenter : X → 𝕜) x : 𝕜) ((↑(Fintype.card X) : 𝕜)⁻¹ : 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
X : Type u_2
inst : Fintype X
𝕜 : Type u_5
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : Nonempty X
inst_5 : DecidableEq X
simp :
  (↑barycenter : X → 𝕜) =
    HSMul.hSMul (β := (j : X) → 𝕜) (HSMul.hSMul (β := 𝕜) (Fintype.card X) 1)⁻¹
      (∑ x : X, HSMul.hSMul (α := 𝕜) (β := (j : X) → 𝕜) 1 (Pi.single (M := fun (j : X) ↦ 𝕜) x 1))
⊢ Eq (α := X → 𝕜) (↑barycenter : X → 𝕜)
    (Finset.centerMass (R := 𝕜) Finset.univ (fun (x : X) ↦ 1) fun (i : X) ↦ Pi.single (M := fun (j : X) ↦ 𝕜) i 1)

Tactic:
simp only [Finset.centerMass, Finset.sum_const, Finset.card_univ]

Premises used: Finset.card_univ, Finset.centerMass, Finset.sum_const
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
X : Type u_2
inst : Fintype X
𝕜 : Type u_5
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : Nonempty X
inst_5 : DecidableEq X
h :
  ∀ (x : X),
    (↑barycenter : X → 𝕜) x =
      HSMul.hSMul (β := (j : X) → 𝕜) (HSMul.hSMul (β := 𝕜) (Fintype.card X) 1)⁻¹
        (∑ x : X, HSMul.hSMul (α := 𝕜) (β := (j : X) → 𝕜) 1 (Pi.single (M := fun (j : X) ↦ 𝕜) x 1)) x
⊢ (↑barycenter : X → 𝕜) =
    HSMul.hSMul (β := (j : X) → 𝕜) (HSMul.hSMul (β := 𝕜) (Fintype.card X) 1)⁻¹
      (∑ x : X, HSMul.hSMul (α := 𝕜) (β := (j : X) → 𝕜) 1 (Pi.single (M := fun (j : X) ↦ 𝕜) x 1))

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
X : Type u_2
inst : Fintype X
𝕜 : Type u_5
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : Nonempty X
inst_5 : DecidableEq X
x : X
⊢ (↑barycenter : X → 𝕜) x =
    HSMul.hSMul (β := (j : X) → 𝕜) (HSMul.hSMul (β := 𝕜) (Fintype.card X) 1)⁻¹
      (∑ x : X, HSMul.hSMul (α := 𝕜) (β := (j : X) → 𝕜) 1 (Pi.single (M := fun (j : X) ↦ 𝕜) x 1)) x

Tactic:
simp [barycenter, Pi.smul_apply, Finset.sum_apply, Pi.single_apply]

Premises used: Pi.single_apply, Finset.sum_apply, stdSimplex.barycenter, Pi.smul_apply
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
rw : ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, z} : Set E) x
⊢ ¬Disjoint (segment 𝕜 u v) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, z})

Tactic:
rw [not_disjoint_iff]

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
obtain :
  ∀ (az bz : 𝕜) (haz : 0 ≤ az) (hbz : 0 ≤ bz) (habz : az + bz = 1),
    ∃ x_1 ∈ segment 𝕜 u v,
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
⊢ ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, z} : Set E) x

Tactic:
obtain ⟨az, bz, haz, hbz, habz, rfl⟩ := hz

Premises used: rfl