awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ B N

Tactic:
simp [B, N, Nat.lt_floor_add_one]

Premises used: Nat.lt_floor_add_one
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ y ∈ B N

Tactic:
have hN : y ∈ B N := by simp [B, N, Nat.lt_floor_add_one]
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
suffices : y ∈ frontier (s ∩ B N) ∩ B N
⊢ y ∈ frontier (s ∩ B N)

Tactic:
suffices y ∈ frontier (s ∩ B N) ∩ B N from this.1
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
rw : y ∈ frontier s ∩ ball x (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
⊢ y ∈ frontier (s ∩ B N) ∩ B N

Tactic:
rw [frontier_inter_open_inter isOpen_ball]

Premises used: Metric.isOpen_ball, frontier_inter_open_inter
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)

Tactic:
⟨hy, hN⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
hN : y ∈ B N
⊢ y ∈ frontier s ∩ ball x (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)

Tactic:
exact ⟨hy, hN⟩
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
inr :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → IsBounded t → μ (frontier t) = 0 by
    let B : ℕ → Set E := fun n => ball x (n + 1)
    have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 := by
      refine measure_iUnion_null fun n =>
        H _ (hs.inter (convex_ball _ _)) ?_ (isBounded_ball.subset inter_subset_right)
      rw [interior_inter, isOpen_ball.interior_eq]
      exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
    refine measure_mono_null (fun y hy => ?_) this; clear this
    set N : ℕ := ⌊dist y x⌋₊
    refine mem_iUnion.2 ⟨N, ?_⟩
    have hN : y ∈ B N := by simp [B, N, Nat.lt_floor_add_one]
    suffices y ∈ frontier (s ∩ B N) ∩ B N from this.1
    rw [frontier_inter_open_inter isOpen_ball]
    exact ⟨hy, hN⟩
-- Module: Mathlib.Analysis.Convex.Measure
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 : Bornology.IsBounded s
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
replace hb : μ (interior s) ≠ ∞ := (hb.subset interior_subset).measure_lt_top.ne
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
rwa₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) =
    0
rwa₂ rwa₃ rwa₄ rwa₅ :
  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∞)

Tactic:
rwa [frontier, measure_diff interior_subset_closure isOpen_interior.nullMeasurableSet hb,
      tsub_eq_zero_iff_le]

Premises used: frontier, isOpen_interior, IsOpen.nullMeasurableSet, tsub_eq_zero_iff_le, MeasureTheory.measure_diff, interior_subset_closure
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
inr :
  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∞)

Tactic:
suffices μ (closure s) ≤ μ (interior s) by
    rwa [frontier, measure_diff interior_subset_closure isOpen_interior.nullMeasurableSet hb,
      tsub_eq_zero_iff_le]
-- Module: Mathlib.Analysis.Convex.Measure
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∞)

Tactic:
(measure_mono <|
      hs.closure_subset_image_homothety_interior_of_one_lt hx r hr).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.measure_mono, Convex.closure_subset_image_homothety_interior_of_one_lt, NNReal.toReal
-- Module: Mathlib.Analysis.Convex.Measure
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
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∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] 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 ?_

Premises used: LE.le.trans_eq, MeasureTheory.measure_mono, Convex.closure_subset_image_homothety_interior_of_one_lt, NNReal.toReal
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
rw₃ 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∞)
⊢ (μ : (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:
rw [addHaar_image_homothety, ← NNReal.coe_pow, NNReal.abs_eq, ENNReal.ofReal_coe_nnreal]

Premises used: NNReal.abs_eq, NNReal.coe_pow, ENNReal.ofReal_coe_nnreal, MeasureTheory.Measure.addHaar_image_homothety
-- Module: Mathlib.Analysis.Convex.Measure
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),
    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]
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
⊢ ∀ᶠ (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
-- Module: Mathlib.Analysis.Convex.Measure
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∞)

Tactic:
ge_of_tendsto ?_ this

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞)

Tactic:
refine ge_of_tendsto ?_ this

Premises used: ge_of_tendsto
-- Module: Mathlib.Analysis.Convex.Measure
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∞)

Tactic:
(((ENNReal.continuous_mul_const hb).comp
    (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ ?_).mono_left nhdsWithin_le_nhds

Premises used: ENNReal.ofNNReal, Continuous.comp, WithTop.some, ENNReal.continuous_mul_const, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Continuous.tendsto', ENNReal.continuous_coe, continuous_pow
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
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∞)
⊢ 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 (((ENNReal.continuous_mul_const hb).comp
    (ENNReal.continuous_coe.comp (continuous_pow d))).tendsto' _ _ ?_).mono_left nhdsWithin_le_nhds

Premises used: Continuous.comp, ENNReal.continuous_mul_const, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Continuous.tendsto', ENNReal.continuous_coe, continuous_pow
-- Module: Mathlib.Analysis.Convex.Measure
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∞)
⊢ 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:
simp
-- Module: Mathlib.Analysis.Convex.Measure
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 : Set E
hs : Convex ℝ s
⊢ NullMeasurableSet s μ

Tactic:
nullMeasurableSet_of_null_frontier (hs.addHaar_frontier μ)

Premises used: Convex.addHaar_frontier, nullMeasurableSet_of_null_frontier
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
ι : Type u_3
f : StdSimplex ℝ ι
x y : ι → X
⊢ dist (iConvexComb f x) (iConvexComb f y) ≤ iConvexComb f fun (i : ι) ↦ dist (x i) (y i)

Tactic:
simpa [iConvexComb_map, Finsupp.sum_mapDomain_index, add_mul]
    using IsConvexDist.dist_iConvexComb_fst_snd_le (f.map fun i ↦ (x i, y i))

Premises used: add_mul, Finsupp.sum_mapDomain_index, Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le, Prod.mk, Convexity.StdSimplex.map, Convexity.iConvexComb_map
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
f : StdSimplex ℝ I
g : I → X
x : X
⊢ dist (iConvexComb f g) x ≤ iConvexComb f fun (i : I) ↦ dist (g i) x

Tactic:
simpa using dist_iConvexComb_le f g (fun _ ↦ x)

Premises used: Convexity.dist_iConvexComb_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x : X
f : StdSimplex ℝ I
g : I → X
⊢ dist x (iConvexComb f g) ≤ iConvexComb f fun (i : I) ↦ dist x (g i)

Tactic:
simpa using dist_iConvexComb_le f (fun _ ↦ x) g

Premises used: Convexity.dist_iConvexComb_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
f : StdSimplex ℝ X
x : X
⊢ dist (sConvexComb f) x ≤ iConvexComb f fun (x_1 : X) ↦ dist x_1 x

Tactic:
simpa using dist_iConvexComb_left_le f id x

Premises used: id, Convexity.dist_iConvexComb_left_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
x : X
f : StdSimplex ℝ X
⊢ dist x (sConvexComb f) ≤ iConvexComb f (dist x)

Tactic:
simpa using dist_iConvexComb_right_le x f id

Premises used: id, Convexity.dist_iConvexComb_right_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
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

Tactic:
(H ..).antisymm ?_

Premises used: LE.le.antisymm
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
refine : t * dist x y ≤ dist (convexCombPair s t hs ht h x y) x
⊢ dist (convexCombPair s t hs ht h x y) x = t * dist x y

Tactic:
refine (H ..).antisymm ?_

Premises used: LE.le.antisymm