awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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 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)
Tactic: classical
  letI := hs.fintype
  rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
  apply congr_arg
  aesop
-- 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
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)
⊢ 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 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: classical
  letI := hs.fintype
  rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
  apply congr_arg
  aesop
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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 (stdSimplex 𝕜 ι)
have rw : IsClosed (X := ι → 𝕜) ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1})
Tactic: rw [stdSimplex_eq_inter]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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 := ι → 𝕜) ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1})
have h₁ : IsClosed (X := ι → 𝕜) (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x})
Tactic: apply IsClosed.inter
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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})
⊢ IsClosed (X := ι → 𝕜) ((⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x}) ∩ {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1})
have h₂ : IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | Eq.{u_1 + 1} (α := 𝕜) (∑ x : ι, f x) 1}
Tactic: apply IsClosed.inter
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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 := ι → 𝕜) (⋂ (x : ι), {f : ι → 𝕜 | 0 ≤ f x})
have h₁ : ∀ (i : ι), IsClosed (X := ι → 𝕜) {f : ι → 𝕜 | 0 ≤ f i}
Tactic: apply isClosed_iInter
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ Membership.mem (γ := Set (ι → ℝ)) (Metric.closedBall 0 1) f
have rw : ∀ (b : ι), dist (f b) (0 b) ≤ 1
Tactic: rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (0 x) ≤ 1
have rw : f x ≤ 1
Tactic: rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Continuous (X := (↑unitInterval : Type)) (Equiv.invFun (stdSimplexEquivIcc ℝ))
have h : Continuous (Y := Fin 2 → ℝ) fun (x : (↑unitInterval : Type)) ↦ ![1 - (↑x : ℝ), (↑x : ℝ)]
Tactic: apply Continuous.subtype_mk
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
x : ι → ℝ
hx : x ∈ stdSimplex ℝ ι
y : ι → ℝ
hy : y ∈ stdSimplex ℝ ι
i : ι
⊢ dist (x i) (y i) ≤ 1
have hx₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) (x i)
Tactic: have hx := mem_Icc_of_mem_stdSimplex hx i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
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)
⊢ dist (x i) (y i) ≤ 1
have hy₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) (y i)
Tactic: have hy := mem_Icc_of_mem_stdSimplex hy i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
h : IsEmpty ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0
have inl : Metric.diam.{u_1} (α := ι → ℝ) ∅ = 0
Tactic: rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
h : IsEmpty ι
inl : Metric.diam.{u_1} (α := ι → ℝ) ∅ = 0
⊢ Metric.diam (stdSimplex ℝ ι) = 0
have inl₁ : Eq (α := ℝ) 0 0
Tactic: rw [stdSimplex_of_isEmpty_index, Metric.diam_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
h : Nonempty ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0
have inr : Metric.diam (α := ι → ℝ) {fun (x : ι) ↦ 1} = 0
Tactic: rw [stdSimplex_unique, Metric.diam_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
h : Nonempty ι
inr : Metric.diam (α := ι → ℝ) {fun (x : ι) ↦ 1} = 0
⊢ Metric.diam (stdSimplex ℝ ι) = 0
have inr₁ : Eq (α := ℝ) 0 0
Tactic: rw [stdSimplex_unique, Metric.diam_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Subsingleton ι
⊢ Metric.diam (stdSimplex ℝ ι) = 0
have x : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
⊢ Metric.diam (stdSimplex ℝ ι) = 1
have refine : 1 ≤ Metric.diam (stdSimplex ℝ ι)
Tactic: refine le_antisymm diam_stdSimplex_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)
have obtain : ∀ (i j : ι) (hij : i ≠ j), 1 ≤ Metric.diam (stdSimplex ℝ ι)
Tactic: obtain ⟨i, j, hij⟩ := exists_pair_ne ι
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)
have rw : dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 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]]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)
have rw : dist (α := (j : ι) → ℝ) (Pi.single (M := fun (a : ι) ↦ ℝ) i 1) (Pi.single (M := fun (j : ι) ↦ ℝ) j 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 _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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 = t
have a : (↑s : X → S) = (↑t : X → S)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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) (1 : S)
have rw : LE.le.{u_1} (α := S) ((s : (a : X) → S) x : S) (∑ x : X, (s : (a : X) → S) x : S)
Tactic: rw [← sum_eq_one s]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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)
have refine_1 : ∀ (y : Y), LE.le.{u_1} (α := S) (0 : S) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s y : S)
Tactic: refine ⟨fun y ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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)
⊢ Membership.mem (α := Y → S) (stdSimplex S Y) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s : Y → S)
have refine_2 : Eq.{u_1 + 1} (α := S) (∑ x : Y, (FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s x) 1
Tactic: refine ⟨fun y ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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
⊢ LE.le.{u_1} (α := S) (0 : S) ((FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s y : S)
have refine_1 : 0 ≤ Finset.sum {x : X | f x = y} s
Tactic: rw [FunOnFinite.linearMap_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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, (FunOnFinite.linearMap S S f : (a : X → S) → Y → S) s x) 1
have refine_2 : Eq.{u_1 + 1} (α := S) (∑ x : Y, Finset.sum {x_1 : X | f x_1 = x} s) (∑ x : X, s x)
Tactic: simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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
⊢ (⇑(FunOnFinite.linearMap S S f) : (a : X → S) → Y → S) '' stdSimplex S X ⊆ stdSimplex S Y
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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)
⊢ (⇑(FunOnFinite.linearMap S S f) : (a : X → S) → Y → S) '' stdSimplex S X ⊆ stdSimplex S Y
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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)
⊢ (⇑(FunOnFinite.linearMap S S f) : (a : X → S) → Y → S) '' stdSimplex S X ⊆ stdSimplex S Y
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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))
⊢ Eq (α := (↑(stdSimplex S Z) : Type (max u_1 u_4))) (map g (map f x)) (map (g ∘ f) x)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
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)
⊢ x = y
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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)
⊢ x = y
have by_contra! : ∀ (this : x ≠ y), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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 : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y
have 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
Tactic: obtain ⟨x, y, hxy⟩ := exists_pair_ne X
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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 : (↑(stdSimplex S X) : Type (max u_1 u_2))) (y : (↑(stdSimplex S X) : Type (max u_1 u_2))), x ≠ y
have 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
Tactic: classical
    obtain ⟨x, y, hxy⟩ := exists_pair_ne X
    exact ⟨vertex x, vertex y, fun h ↦ hxy (vertex_injective h)⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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))
⊢ s = t
have h : ∀ (i : X), Eq.{u_1 + 1} (α := S) ((s : (a : X) → S) i : S) ((t : (a : X) → S) i : S)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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)
have 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)
Tactic: rw [← sum_eq_one u, Finset.sum_eq_single i _ (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := S) ((s : (a : X) → S) i : S) ((t : (a : X) → S) i : S)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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
⊢ Eq.{u_1 + 1} (α := S) ((s : (a : X) → S) x : S) (1 : S)
have obtain : Eq.{u_1 + 1} (α := S) ((default : (a : X) → S) x : S) (1 : S)
Tactic: obtain rfl : s = default := by subsingleton
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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
⊢ Eq (α := X → 𝕜) (↑barycenter : X → 𝕜)
    (Finset.centerMass (R := 𝕜) Finset.univ (fun (x : X) ↦ 1) fun (i : X) ↦ Pi.single (M := fun (j : X) ↦ 𝕜) i 1)
have 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))
Tactic: simp only [Finset.centerMass, Finset.sum_const, Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StdSimplex (goal)
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
⊢ (↑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))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ¬Disjoint (segment 𝕜 u v) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, z})
have rw : ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, z} : Set E) x
Tactic: rw [not_disjoint_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, z} : Set E) x
have 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
Tactic: obtain ⟨az, bz, haz, hbz, habz, rfl⟩ := hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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 : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
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
have inl : ∀ (haz : LE.le.{u_1} (α := 𝕜) 0 0) (habz : 0 + bz = 1),
  ∃ x_1 ∈ segment 𝕜 u v,
    Membership.mem (γ := Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + bz • y} : Set E) x_1
Tactic: obtain rfl | haz' := haz.eq_or_lt
Cleared hypotheses: az, haz, habz