awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rwa : Eq (α := ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s \ interior s) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rwa [frontier, measure_diff interior_subset_closure isOpen_interior.nullMeasurableSet hb,
      tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
rwa :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s \ interior s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rwa₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
  0
Tactic: rwa [frontier, measure_diff interior_subset_closure isOpen_interior.nullMeasurableSet hb,
      tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: suffices μ (closure s) ≤ μ (interior s) by
    rwa [frontier, measure_diff interior_subset_closure isOpen_interior.nullMeasurableSet hb,
      tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have refine : (μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x (↑r : ℝ)) : (a : E) → E) '' interior s) =
  HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: refine (measure_mono <|
      hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x (↑r : ℝ)) : (a : E) → E) '' interior s) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑r : ℝ) ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑r : ℝ) ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x (↑r : ℝ)) : (a : E) → E) '' interior s) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑(r ^ finrank ℝ E) : ℝ)|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑r : ℝ) ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑(r ^ finrank ℝ E) : ℝ)|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x (↑r : ℝ)) : (a : E) → E) '' interior s) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have rw₂ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (↑(r ^ finrank ℝ E) : ℝ)) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
r : ℝ≥0
hr : 1 < r
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑r : ℝ) ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(↑(r ^ finrank ℝ E) : ℝ)|) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
rw₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (↑(r ^ finrank ℝ E) : ℝ)) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x (↑r : ℝ)) : (a : E) → E) '' interior s) =
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have rw₃ : HMul.hMul (β := ℝ≥0∞) (↑(r ^ finrank ℝ E) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have this : ∀ (r : ℝ≥0),
  1 < r →
    (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: have : ∀ r : ℝ≥0, 1 < r → μ (closure s) ≤ ↑(r ^ d) * μ (interior s) := fun r hr ↦ by
    refine (measure_mono <|
      hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq ?_
    rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
this :
  ∀ (r : ℝ≥0),
    1 < r →
      (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have this₁ : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1,
  (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: have : ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1, μ (closure s) ≤ ↑(r ^ d) * μ (interior s) :=
    mem_of_superset self_mem_nhdsWithin this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
this_1 :
  ∀ (r : ℝ≥0),
    1 < r →
      (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
this :
  ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1,
    (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
have inr : Tendsto (β := ℝ≥0∞)
  (fun (c : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑(c ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)) (𝓝[>] 1)
  (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (interior s)) : Filter ℝ≥0∞)
Tactic: refine ge_of_tendsto ?_ this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
d : ℕ := finrank ℝ E
this_1 :
  ∀ (r : ℝ≥0),
    1 < r →
      (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
this :
  ∀ᶠ (r : ℝ≥0) in 𝓝[>] 1,
    (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(r ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (c : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑(c ^ d) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)) (𝓝[>] 1)
    (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (interior s)) : Filter ℝ≥0∞)
have inr : Eq (α := ℝ≥0∞)
  (Function.comp (α := ℝ≥0) (fun (x : ℝ≥0∞) ↦ HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞))
      (ENNReal.ofNNReal ∘ fun (a : ℝ≥0) ↦ a ^ d) 1 :
    ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)
Tactic: refine (((ENNReal.continuous_mul_const hb).comp
    (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ ?_).mono_left nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y
have refine : t * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
Tactic: refine (H ..).antisymm ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
| t * dist x y
have rw : dist x y - s * dist x y
Tactic: rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ t * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have conv_lhs : dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
Tactic: conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
Tactic: grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have grw₁ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + s * dist y x
Tactic: grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
grw₁ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + s * dist y x
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have grw₂ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs sorry y x) y
Tactic: grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
grw₁ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + s * dist y x
grw₂ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have grw₃ : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs sorry y x) y
Tactic: grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
grw₁ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + s * dist y x
grw₂ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
grw₃ : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have grw₄ : dist x y ≤ dist (convexCombPair t s ht hs sorry y x) x + dist (convexCombPair t s ht hs sorry y x) y
Tactic: grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
H :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
grw : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + s * dist x y
grw₁ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + s * dist y x
grw₂ : dist y x ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
grw₃ : dist x y ≤ dist (convexCombPair s t hs ht h x y) x + dist (convexCombPair t s ht hs ⋯ y x) y
grw₄ : dist x y ≤ dist (convexCombPair t s ht hs ⋯ y x) x + dist (convexCombPair t s ht hs ⋯ y x) y
⊢ dist x y - s * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
have grw₅ : dist x y ≤ dist x y
Tactic: grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y
have suffices : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
Tactic: suffices H : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
      dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y by
    refine (H ..).antisymm ?_
    conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
    grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s_1 t_1 : ℝ
hs_1 : 0 ≤ s_1
ht_1 : 0 ≤ t_1
h_1 : s_1 + t_1 = 1
x_1 y_1 : X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
have grw : (iConvexComb (StdSimplex.duple x y hs ht h) fun (x_2 : X) ↦ dist x_2 x) ≤ t * dist x y
Tactic: grw [convexCombPair, dist_sConvexComb_left_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y
have suffices : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X), dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
Tactic: classical
  suffices H : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
      dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y by
    refine (H ..).antisymm ?_
    conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
    grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
  intro s t hs ht h x y
  grw [convexCombPair, dist_sConvexComb_left_le]
  simp [iConvexComb_eq_sum, Finsupp.sum_add_index, add_mul, dist_comm y x]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : X
suffices suffices₁ suffices₂ suffices₃ :
  ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
    dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y
have suffices₄ : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
  (iConvexComb (StdSimplex.duple x y hs ht h) fun (x_1 : X) ↦ dist x_1 x) ≤ t * dist x y
Tactic: classical
  suffices H : ∀ {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X),
      dist (convexCombPair s t hs ht h x y) x ≤ t * dist x y by
    refine (H ..).antisymm ?_
    conv_lhs => rw [eq_sub_iff_add_eq'.mpr h, sub_mul, one_mul]
    grw [sub_le_iff_le_add, dist_comm x y, ← H ht hs ((add_comm _ _).trans h) y x, dist_comm,
      convexCombPair_symm, ← dist_triangle_left]
  intro s t hs ht h x y
  grw [convexCombPair, dist_sConvexComb_left_le]
  simp [iConvexComb_eq_sum, Finsupp.sum_add_index, add_mul, dist_comm y x]