awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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, Finset.centerMass_mem_convexHull
-- 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:
convexHull_basis_eq_stdSimplex R ι

Premises used: convexHull_basis_eq_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 ι
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)
⊢ (convexHull R : (a : Set ((j : ι) → R)) → Set ((j : ι) → R))
      (range fun (i : ι) ↦ Pi.single (M := fun (a : ι) ↦ R) i 1) =
    stdSimplex R ι

Tactic:
convert! convexHull_basis_eq_stdSimplex R ι

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

Tactic:
rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]

Premises used: Set.range_comp, convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull
-- Module: Mathlib.Analysis.Convex.StdSimplex
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)
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)
⊢ 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:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Analysis.Convex.StdSimplex
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)
⊢ 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:
aesop
-- Module: Mathlib.Analysis.Convex.StdSimplex
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
letI letI₁ letI₂ :
  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)
letI₃ :
  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)
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)
⊢ 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)

Tactic:
classical
  letI := hs.fintype
  rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
  apply congr_arg
  aesop

Premises used: Set.range_comp, convexHull_basis_eq_stdSimplex, congr_arg, LinearMap.image_convexHull
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
rw : IsClosed (X := ι → 𝕜) ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1})
⊢ IsClosed (stdSimplex 𝕜 ι)

Tactic:
rw [stdSimplex_eq_inter]

Premises used: stdSimplex_eq_inter
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
h₁ : IsClosed (X := ι → 𝕜) (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x})
h₂ : IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1}
⊢ IsClosed (X := ι → 𝕜) ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1})

Tactic:
apply IsClosed.inter

Premises used: IsClosed.inter
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
h₁ : ∀ (i : ι), IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | 0 ≤ f i}
⊢ IsClosed (X := ι → 𝕜) (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x})

Tactic:
apply isClosed_iInter

Premises used: isClosed_iInter
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
⊢ ∀ (i : ι), IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | 0 ≤ f i}

Tactic:
fun i ↦ isClosed_le continuous_const (continuous_apply i)

Premises used: continuous_const, setOf, isClosed_le, continuous_apply
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
⊢ ∀ (i : ι), IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | 0 ≤ f i}

Tactic:
exact fun i ↦ isClosed_le continuous_const (continuous_apply i)

Premises used: continuous_const, isClosed_le, continuous_apply
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
⊢ Continuous (Y := 𝕜) fun (f : ι → 𝕜) ↦ ∑ x : ι, f x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
⊢ IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1}

Tactic:
exact isClosed_eq (by fun_prop) continuous_const

Premises used: continuous_const, isClosed_eq
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
inst_6 : CompactIccSpace 𝕜
inst_7 : IsOrderedAddMonoid 𝕜
⊢ IsCompact (stdSimplex 𝕜 ι)

Tactic:
IsCompact.of_isClosed_subset isCompact_Icc (isClosed_stdSimplex 𝕜 ι) (stdSimplex_subset_Icc 𝕜)

Premises used: isClosed_stdSimplex, CompactIccSpace.isCompact_Icc, IsCompact.of_isClosed_subset, stdSimplex_subset_Icc
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : TopologicalSpace 𝕜
inst_2 : Semiring 𝕜
inst_3 : PartialOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : ContinuousAdd 𝕜
inst_6 : CompactIccSpace 𝕜
inst_7 : IsOrderedAddMonoid 𝕜
⊢ CompactSpace (↑(stdSimplex 𝕜 ι) : Type (max u_1 u_2))

Tactic:
isCompact_iff_compactSpace.mp <| isCompact_stdSimplex 𝕜 _

Premises used: isCompact_stdSimplex, isCompact_iff_compactSpace, Iff.mp
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
rw : ∀ (b : ι), dist (f b) (0 b) ≤ 1
⊢ Membership.mem (γ := Set (ι → ℝ)) (Metric.closedBall 0 1) f

Tactic:
rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]

Premises used: dist_pi_le_iff, zero_le_one, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
rw : f x ≤ 1
⊢ dist (f x) (0 x) ≤ 1

Tactic:
rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]

Premises used: Pi.zero_apply, And.left, Real.dist_0_eq_abs, abs_of_nonneg
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1

Tactic:
(mem_Icc_of_mem_stdSimplex hf x).2

Premises used: mem_Icc_of_mem_stdSimplex, And.right
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1

Tactic:
exact (mem_Icc_of_mem_stdSimplex hf x).2

Premises used: mem_Icc_of_mem_stdSimplex, And.right
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
⊢ IsBounded (stdSimplex ℝ ι)

Tactic:
(Metric.isBounded_iff_subset_closedBall 0).2 ⟨1, stdSimplex_subset_closedBall⟩

Premises used: Iff.mpr, stdSimplex_subset_closedBall, Exists.intro, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
⊢ (stdSimplex ℝ ι).Nonempty

Tactic:
⟨_, single_mem_stdSimplex ℝ (Classical.arbitrary ι)⟩

Premises used: Real, single_mem_stdSimplex, Set.Nonempty, Exists.intro, Classical.arbitrary
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
⊢ (stdSimplex ℝ ι).Nonempty

Tactic:
exact ⟨_, single_mem_stdSimplex ℝ (Classical.arbitrary ι)⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
⊢ (stdSimplex ℝ ι).Nonempty

Tactic:
classical
    exact ⟨_, single_mem_stdSimplex ℝ (Classical.arbitrary ι)⟩
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
⊢ PathConnectedSpace.{u_1} (↑(stdSimplex ℝ ι) : Type u_1)

Tactic:
isPathConnected_iff_pathConnectedSpace.1 (isPathConnected_stdSimplex _)

Premises used: isPathConnected_stdSimplex, Iff.mp, isPathConnected_iff_pathConnectedSpace
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
h : Continuous (Y := Fin 2 → ℝ) fun (x : (↑unitInterval : Type)) ↦ ![1 - (↑x : ℝ), (↑x : ℝ)]
⊢ Continuous (X := (↑unitInterval : Type)) (Equiv.invFun (stdSimplexEquivIcc ℝ))

Tactic:
apply Continuous.subtype_mk

Premises used: Continuous.subtype_mk
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Continuous (Y := Fin 2 → ℝ) fun (x : (↑unitInterval : Type)) ↦ ![1 - (↑x : ℝ), (↑x : ℝ)]

Tactic:
(continuous_pi <| Fin.forall_fin_two.2
      ⟨continuous_const.sub continuous_subtype_val, continuous_subtype_val⟩)

Premises used: Fin.forall_fin_two, Iff.mpr, continuous_subtype_val, continuous_const, continuous_pi, And.intro, Continuous.sub
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Continuous (Y := Fin 2 → ℝ) fun (x : (↑unitInterval : Type)) ↦ ![1 - (↑x : ℝ), (↑x : ℝ)]

Tactic:
exact (continuous_pi <| Fin.forall_fin_two.2
      ⟨continuous_const.sub continuous_subtype_val, continuous_subtype_val⟩)

Premises used: Fin.forall_fin_two, Iff.mpr, continuous_pi, And.intro
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
⊢ Eq (α := (↑unitInterval : Type))
    ((stdSimplexHomeomorphUnitInterval : (a : (↑(stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
        (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) ⋯) :
      (↑unitInterval : Type))
    (0 : (↑unitInterval : Type))

Tactic:
rfl

Premises used: Function.update, Set.Mem, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
⊢ Eq (α := (↑unitInterval : Type))
    ((stdSimplexHomeomorphUnitInterval : (a : (↑(stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
        (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) ⋯) :
      (↑unitInterval : Type))
    (1 : (↑unitInterval : Type))

Tactic:
rfl

Premises used: Function.update, Set.Mem, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
hx : x ∈ stdSimplex ℝ ι
y : ι → ℝ
hy : y ∈ stdSimplex ℝ ι
i : ι
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (x i)

Tactic:
have hx := mem_Icc_of_mem_stdSimplex hx i
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
hx_1 : x ∈ stdSimplex ℝ ι
y : ι → ℝ
hy : y ∈ stdSimplex ℝ ι
i : ι
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) (x i)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (y i)

Tactic:
have hy := mem_Icc_of_mem_stdSimplex hy i
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
hx_1 : x ∈ stdSimplex ℝ ι
y : ι → ℝ
hy_1 : y ∈ stdSimplex ℝ ι
i : ι
hx : Membership.mem (γ := Set ℝ) (Icc 0 1) (x i)
hy : Membership.mem (γ := Set ℝ) (Icc 0 1) (y i)
⊢ dist (x i) (y i) ≤ 1

Tactic:
grind [Real.dist_eq]

Premises used: Real.dist_eq
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
h : IsEmpty ι
inl : Metric.diam.{u_1} (α := ι → ℝ) ∅ = 0
inl₁ inl₂ : Eq (α := ℝ) 0 0
⊢ Metric.diam (stdSimplex ℝ ι) = 0

Tactic:
rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]

Premises used: stdSimplex_of_isEmpty_index, Metric.diam_empty
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
h : Nonempty ι
inr : Metric.diam (α := ι → ℝ) {fun (x : ι) ↦ 1} = 0
inr₁ inr₂ : Eq (α := ℝ) 0 0
⊢ Metric.diam (stdSimplex ℝ ι) = 0

Tactic:
rw [stdSimplex_unique, Metric.diam_singleton]

Premises used: Metric.diam_singleton, stdSimplex_unique
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
⊢ IsEmpty ι ∨ Nonempty ι

Tactic:
cases isEmpty_or_nonempty ι with
  | inl h => rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]
  | inr h => rw [stdSimplex_unique, Metric.diam_singleton]

Premises used: stdSimplex_of_isEmpty_index, isEmpty_or_nonempty, Metric.diam_singleton, Metric.diam_empty, stdSimplex_unique
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
⊢ Metric.diam (stdSimplex ℝ ι) = 1

Tactic:
le_antisymm diam_stdSimplex_le ?_

Premises used: diam_stdSimplex_le, le_antisymm
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
refine : 1 ≤ Metric.diam (stdSimplex ℝ ι)
⊢ Metric.diam (stdSimplex ℝ ι) = 1

Tactic:
refine le_antisymm diam_stdSimplex_le ?_

Premises used: diam_stdSimplex_le, le_antisymm
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
obtain : ∀ (i j : ι) (hij : i ≠ j), 1 ≤ Metric.diam (stdSimplex ℝ ι)
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
obtain ⟨i, j, hij⟩ := exists_pair_ne ι

Premises used: exists_pair_ne
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 = dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 1)

Tactic:
simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]

Premises used: dist_single_single, Real.dist_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
rw :
  dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 1) ≤
    Metric.diam (stdSimplex ℝ ι)
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
rw [show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]]
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 1) ≤
    Metric.diam (stdSimplex ℝ ι)

Tactic:
Metric.dist_le_diam_of_mem (bounded_stdSimplex _)
    (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

Premises used: single_mem_stdSimplex, bounded_stdSimplex, Metric.dist_le_diam_of_mem
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 1) ≤
    Metric.diam (stdSimplex ℝ ι)

Tactic:
exact Metric.dist_le_diam_of_mem (bounded_stdSimplex _)
    (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

Premises used: single_mem_stdSimplex, Metric.dist_le_diam_of_mem
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
rw rw₁ rw₂ :
  dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 1) ≤
    Metric.diam (stdSimplex ℝ ι)
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
classical
  rw [show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]]
  exact Metric.dist_le_diam_of_mem (bounded_stdSimplex _)
    (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

Premises used: single_mem_stdSimplex, Metric.dist_le_diam_of_mem
-- 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
⊢ Function.Injective (β := (a : X) → S) fun (s : (↑(stdSimplex S X) : Type (max u_1 u_2))) ↦ (↑s : X → S)

Tactic:
aesop
-- 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
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
h : Eq (α := (a : X) → S) (⇑s : (a : X) → S) (⇑t : (a : X) → S)
a : (↑s : X → S) = (↑t : X → S)
⊢ s = t

Tactic:
ext : 1
-- 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
s t : (↑(stdSimplex S X) : Type (max u_1 u_2))
h : Eq (α := (a : X) → S) (⇑s : (a : X) → S) (⇑t : (a : X) → S)
⊢ (↑s : X → S) = (↑t : X → S)

Tactic:
assumption
-- 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
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
⊢ LE.le.{u_1} (α := S) (0 : S) ((s : (a : X) → S) x : S)

Tactic:
s.2.1 x

Premises used: And.left, Subtype.property
-- 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
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
⊢ Eq.{u_1 + 1} (α := S) (∑ x : X, (s : (a : X) → S) x) 1

Tactic:
s.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Analysis.Convex.StdSimplex
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
s : (↑(stdSimplex S (Fin 2)) : Type u_1)
⊢ HAdd.hAdd (α := S) (β := S) ((s : (a : Fin 2) → S) 0 : S) ((s : (a : Fin 2) → S) 1 : S) = 1

Tactic:
simpa only [Fin.sum_univ_two] using sum_eq_one s

Premises used: stdSimplex.sum_eq_one, Fin.sum_univ_two
-- 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
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
rw : LE.le.{u_1} (α := S) ((s : (a : X) → S) x : S) (∑ x : X, (s : (a : X) → S) x : S)
⊢ LE.le.{u_1} (α := S) ((s : (a : X) → S) x : S) (1 : S)

Tactic:
rw [← sum_eq_one s]

Premises used: 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
inst_2 : Fintype X
inst_3 : IsOrderedRing S
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
⊢ ∀ (i : X), Membership.mem (γ := Finset X) Finset.univ i → LE.le.{u_1} (α := S) (0 : S) ((s : (a : X) → S) i : S)

Tactic:
simp
-- 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
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
⊢ Membership.mem (γ := Finset X) Finset.univ x

Tactic:
simp
-- 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
s : (↑(stdSimplex S X) : Type (max u_1 u_2))
x : X
⊢ LE.le.{u_1} (α := S) ((s : (a : X) → S) x : S) (∑ x : X, (s : (a : X) → S) x : S)

Tactic:
simpa only using Finset.single_le_sum (by simp) (by simp)

Premises used: Finset.single_le_sum