awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
A :
  Tendsto
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1)
    (𝓝
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E)))
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have A₁ : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
  (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
Tactic: simp only [one_pow, one_mul, ENNReal.ofReal_one] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have refine : ∀ᶠ (c : ℝ) in 𝓝[<] 1,
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (c ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
    (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)
Tactic: refine le_of_tendsto A ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] 1,
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (c ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
      (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)
have h : ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (Ioo 0 1) r),
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
    (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)
Tactic: filter_upwards [Ioo_mem_nhdsLT zero_lt_one] with r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞))
    (𝓝[<] 1) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) : Filter ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioo 0 1) r
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ≤
    (μ : (a : Set E) → ℝ≥0∞) (ball 0 1)
have h : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: rw [← addHaar_closedBall' μ (0 : E) hr.1.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : 0 ≤ r
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unitBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : 0 ≤ r
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: rw [addHaar_closedBall' μ x hr, addHaar_unitClosedBall_eq_addHaar_unitBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
have pos : ∀ (h : r < 0),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
Tactic: by_cases! h : r < 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
pos :
  ∀ (h : r < 0),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
have neg : ∀ (h : 0 ≤ r),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
Tactic: by_cases! h : r < 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
h : r < 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
Tactic: rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
h : r < 0
pos : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
have pos₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
h : 0 ≤ r
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
have neg : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
  (μ : (a : Set E) → ℝ≥0∞) (ball x r)
Tactic: rw [addHaar_closedBall μ x h, addHaar_ball μ x h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
h : 0 ≤ r
neg :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
    (μ : (a : Set E) → ℝ≥0∞) (ball x r)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
have neg₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: rw [addHaar_closedBall μ x h, addHaar_ball μ x h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : ∀ (h : r < 0), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases hr.lt_or_gt with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
inl : ∀ (h : r < 0), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (h : 0 < r), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases hr.lt_or_gt with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r \ ball x r) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← closedBall_diff_ball,
      measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
        measure_ball_lt_top.ne,
      addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r \ ball x r) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) =
  0
Tactic: rw [← closedBall_diff_ball,
      measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
        measure_ball_lt_top.ne,
      addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r \ ball x r) : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) =
    0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₂ : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)) =
  0
Tactic: rw [← closedBall_diff_ball,
      measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
        measure_ball_lt_top.ne,
      addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r \ ball x r) : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) =
    0
inr₂ :
  HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)) =
    0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₃ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) -
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
  0
Tactic: rw [← closedBall_diff_ball,
      measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
        measure_ball_lt_top.ne,
      addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
x : E
r : ℝ
hr : r ≠ 0
h : 0 < r
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r \ ball x r) : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) =
    0
inr₂ :
  HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)) =
    0
inr₃ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) -
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
    0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₄ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← closedBall_diff_ball,
      measure_diff ball_subset_closedBall measurableSet_ball.nullMeasurableSet
        measure_ball_lt_top.ne,
      addHaar_ball_of_pos μ _ h, addHaar_closedBall μ _ h.le, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x 0) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases eq_or_ne r 0 with (rfl | h)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
r : ℝ
inl : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x 0) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (h : r ≠ 0), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases eq_or_ne r 0 with (rfl | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x 0) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [sphere_zero, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
inst_6 : Nontrivial E
x : E
inl : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x 0) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [sphere_zero, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) *
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))⁻¹ =
    ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) *
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) =
  ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞)
Tactic: rw [ENNReal.mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) =
    ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) *
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))⁻¹ =
    ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞)
have ha : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [ENNReal.mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) =
    ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞)
ha : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) *
      (HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (|r| ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))⁻¹ =
    ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞)
have hb : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [ENNReal.mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have h0 : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0
Tactic: rw [ENNReal.mul_inv_cancel, one_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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
r : ℝ
hr : r ≠ 0
x y : E
s t : Set E
h0 : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ 0
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) * (ENNReal.ofReal (|r| ^ finrank ℝ E))⁻¹ *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) t)⁻¹ : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have ht : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ∞
Tactic: rw [ENNReal.mul_inv_cancel, one_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (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 : Set E
⊢ IsUnifLocDoublingMeasure μ
have refine : ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
  ∀ (x : E),
    (μ : (a : Set E) → ℝ≥0∞) (closedBall x (2 * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
Tactic: refine ⟨⟨(2 : ℝ≥0) ^ finrank ℝ E, ?_⟩⟩