awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 0 ≤ r
s : 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∞) s : ℝ≥0∞)
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∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (r • s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥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∞) s : ℝ≥0∞)
Tactic: rw [addHaar_smul, abs_pow, abs_of_nonneg 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
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
⊢ NullMeasurableSet (r • s) μ
have inl : ∀ (hs : NullMeasurableSet ∅ μ), NullMeasurableSet (HSMul.hSMul (β := Set E) r ∅) μ
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- 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
hs : NullMeasurableSet s μ
r : ℝ
inl : ∀ (hs : NullMeasurableSet ∅ μ), NullMeasurableSet (HSMul.hSMul (β := Set E) r ∅) μ
⊢ NullMeasurableSet (r • s) μ
have inr : ∀ (hs' : s.Nonempty), NullMeasurableSet (r • s) μ
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- 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
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
⊢ NullMeasurableSet (r • s) μ
have inr : NullMeasurableSet (HSMul.hSMul (α := ℝ) 0 s) μ
Tactic: obtain rfl | hr := eq_or_ne r 0
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
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
inr : NullMeasurableSet (HSMul.hSMul (α := ℝ) 0 s) μ
⊢ NullMeasurableSet (r • s) μ
have inr₁ : ∀ (hr : r ≠ 0), NullMeasurableSet (r • s) μ
Tactic: obtain rfl | hr := eq_or_ne 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
s : Set E
hs : NullMeasurableSet s μ
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
⊢ NullMeasurableSet (r • s) μ
have inr : ∀ (t : Set E) (ht : MeasurableSet t) (hst : s =ᶠ[ae μ] t), NullMeasurableSet (r • s) μ
Tactic: obtain ⟨t, ht, hst⟩ := hs
Cleared hypotheses: hs
-- 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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ NullMeasurableSet (r • s) μ
have inr : r • s =ᶠ[ae μ] r • t
Tactic: refine ⟨_, ht.const_smul_of_ne_zero 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
s : Set E
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ r • s =ᶠ[ae μ] r • t
have inr : ∀ (hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_symmDiff_eq_zero_iff] at hst ⊢
Cleared hypotheses: hst
-- 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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (r • symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]
-- 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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (r • symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) = 0
Tactic: rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]
-- 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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (r • symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₂ : ENNReal.ofReal |r ^ finrank ℝ E| * 0 = 0
Tactic: rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]
-- 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
r : ℝ
hs' : s.Nonempty
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (r • symmDiff s t) : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |r ^ finrank ℝ E|) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff s t) : ℝ≥0∞) = 0
inr₂ : ENNReal.ofReal |r ^ finrank ℝ E| * 0 = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (symmDiff (r • s) (r • t)) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← smul_set_symmDiff₀ hr, addHaar_smul μ, hst, mul_zero]
-- 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 : ℝ
s : Set E
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x r) : (a : E) → E) '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (y : E) ↦ y + x) '' HSMul.hSMul (β := Set E) r ((fun (y : E) ↦ y + -x) '' s)) :
      ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⇑(AffineMap.homothety x r) : (a : E) → E) '' s) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ r • (x_1 - x) + x) '' s) : ℝ≥0∞)
Tactic: simp only [← image_smul, image_image, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 r) : ℝ≥0∞)
have this : Eq (α := Set E) (ball 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r)
Tactic: have : ball (0 : E) r = (x + ·) ⁻¹' ball x r := by simp [preimage_add_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
this : Eq (α := Set E) (ball 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 r) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r) : ℝ≥0∞)
Tactic: rw [this, measure_preimage_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
this : Eq (α := Set E) (ball 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' ball x r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 r) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
Tactic: rw [this, measure_preimage_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)
have this : Eq (α := Set E) (closedBall 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r)
Tactic: have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp [preimage_add_closedBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
this : Eq (α := Set E) (closedBall 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r) : ℝ≥0∞)
Tactic: rw [this, measure_preimage_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
μ : Measure E
inst_3 : μ.IsAddHaarMeasure
x : E
r : ℝ
this : Eq (α := Set E) (closedBall 0 r) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' closedBall x r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: rw [this, measure_preimage_add]
-- 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
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
have this : ball 0 (r * s) = HSMul.hSMul (β := Set E) r (ball 0 s)
Tactic: have : ball (0 : E) (r * s) = r • ball (0 : E) s := by
    simp only [_root_.smul_ball hr.ne' (0 : E) s, Real.norm_eq_abs, abs_of_nonneg hr.le, smul_zero]
-- 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∞) (ball x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x (r * 1)) : ℝ≥0∞)
Tactic: rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]
-- 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 : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x (r * 1)) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
Tactic: rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]
-- 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 : ℝ
hr : 0 ≤ r
s : ℝ
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
have inl : ∀ (hr : LE.le (α := ℝ) 0 0),
  (μ : (a : Set E) → ℝ≥0∞) (ball x (0 * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 0 (finrank ℝ E)))
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
Tactic: rcases hr.eq_or_lt with (rfl | h)
Cleared hypotheses: 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
inst_6 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
inl :
  ∀ (hr : LE.le (α := ℝ) 0 0),
    (μ : (a : Set E) → ℝ≥0∞) (ball x (0 * s)) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (HPow.hPow (α := ℝ) 0 (finrank ℝ E)))
        ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
have inr : ∀ (h : 0 < r),
  (μ : (a : Set E) → ℝ≥0∞) (ball x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 s) : ℝ≥0∞)
Tactic: rcases hr.eq_or_lt 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
r : ℝ
hr : 0 ≤ r
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x (r * 1)) : ℝ≥0∞)
Tactic: rw [← addHaar_ball_mul μ x hr, mul_one]
-- 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 : ℝ
hr : 0 ≤ r
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x (r * 1)) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (ball x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)
Tactic: rw [← addHaar_ball_mul μ x hr, mul_one]
-- 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
x : E
r : ℝ
hr : 0 < r
s : ℝ
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 s) : ℝ≥0∞)
have this : closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)
Tactic: have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
    simp [smul_closedBall' hr.ne' (0 : E), abs_of_nonneg hr.le]
-- 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
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
hs : 0 ≤ s
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * s)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 s) : ℝ≥0∞)
have this : closedBall 0 (r * s) = HSMul.hSMul (β := Set E) r (closedBall 0 s)
Tactic: have : closedBall (0 : E) (r * s) = r • closedBall (0 : E) s := by
    simp [smul_closedBall r (0 : E) hs, abs_of_nonneg 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
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∞) (closedBall 0 1) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * 1)) : ℝ≥0∞)
Tactic: rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]
-- 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 :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x (r * 1)) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: rw [← addHaar_closedBall_mul μ x hr zero_le_one, mul_one]
-- 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
⊢ μ.real (closedBall x r) = r ^ finrank ℝ E * μ.real (closedBall 0 1)
have simp : 0 ≤ r ^ finrank ℝ E ∨ ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) = 0
Tactic: simp only [measureReal_def, addHaar_closedBall' μ x hr, ENNReal.toReal_mul, mul_eq_mul_right_iff,
    ENNReal.toReal_ofReal_eq_iff]
-- 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
⊢ 0 ≤ r ^ finrank ℝ E ∨ ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1)) = 0
have h : 0 ≤ r ^ finrank ℝ E
Tactic: left
-- 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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
Tactic: apply le_antisymm _ (measure_mono ball_subset_closedBall)
-- 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
⊢ 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∞)))
have refine : Tendsto (fun (r : ℝ) ↦ ENNReal.ofReal (r ^ finrank ℝ E)) (𝓝[<] 1)
  (𝓝 (ENNReal.ofReal (HPow.hPow (α := ℝ) 1 (finrank ℝ E))))
Tactic: refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)
-- 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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
have 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∞)))
Tactic: have A : Tendsto
      (fun r : ℝ => ENNReal.ofReal (r ^ finrank ℝ E) * μ (closedBall (0 : E) 1)) (𝓝[<] 1)
        (𝓝 (ENNReal.ofReal ((1 : ℝ) ^ finrank ℝ E) * μ (closedBall (0 : E) 1))) := by
    refine ENNReal.Tendsto.mul ?_ (by simp) tendsto_const_nhds (by simp)
    exact ENNReal.tendsto_ofReal ((tendsto_id'.2 nhdsWithin_le_nhds).pow _)