awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
exact measure_mono (closedBall_subset_ball hr.2)

Premises used: Metric.closedBall_subset_ball, And.right, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
rw₁ 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∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x r) =
    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]

Premises used: MeasureTheory.Measure.addHaar_unitClosedBall_eq_addHaar_unitBall, MeasureTheory.Measure.addHaar_closedBall'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 (ball 0 1)

Tactic:
simp [addHaar_real_closedBall' μ x hr, measureReal_def,
    addHaar_unitClosedBall_eq_addHaar_unitBall]

Premises used: MeasureTheory.Measure.addHaar_unitClosedBall_eq_addHaar_unitBall, MeasureTheory.Measure.addHaar_real_closedBall', MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
neg :
  ∀ (h : 0 ≤ r),
    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∞)

Tactic:
by_cases! h : r < 0
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
pos₁ pos₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)

Tactic:
rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]

Premises used: Iff.mpr, LT.lt.le, Metric.closedBall_eq_empty, Metric.ball_eq_empty
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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)
neg₁ 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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball x r) : ℝ≥0∞)

Tactic:
rw [addHaar_closedBall μ x h, addHaar_ball μ x h]

Premises used: MeasureTheory.Measure.addHaar_closedBall, MeasureTheory.Measure.addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 : ℝ
⊢ μ.real (closedBall x r) = μ.real (ball x r)

Tactic:
simp [measureReal_def, addHaar_closedBall_eq_addHaar_ball μ x r]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
inr : ∀ (h : 0 < r), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases hr.lt_or_gt with (h | h)

Premises used: Ne.lt_or_gt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 : r < 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [empty_diff, measure_empty, ← closedBall_diff_ball, closedBall_eq_empty.2 h]

Premises used: Iff.mpr, MeasureTheory.measure_empty, Metric.closedBall_eq_empty, Metric.closedBall_diff_ball, Set.empty_diff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
inr₄ inr₅ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere 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]

Premises used: Metric.ball_subset_closedBall, MeasureTheory.Measure.addHaar_ball_of_pos, MeasurableSet.nullMeasurableSet, tsub_self, LT.lt.le, measurableSet_ball, MeasureTheory.measure_diff, MeasureTheory.measure_ball_lt_top, Metric.closedBall_diff_ball, MeasureTheory.Measure.addHaar_closedBall, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
inr : ∀ (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∞)

Tactic:
rcases eq_or_ne r 0 with (rfl | h)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
inl₁ inl₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sphere x 0) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [sphere_zero, measure_singleton]

Premises used: Metric.sphere_zero, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
addHaar_sphere_of_ne_zero μ x h

Premises used: MeasureTheory.Measure.addHaar_sphere_of_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞) (sphere x r) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact addHaar_sphere_of_ne_zero μ x h

Premises used: MeasureTheory.Measure.addHaar_sphere_of_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • s) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({y} + r • 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∞))⁻¹

Tactic:
simp only [div_eq_mul_inv, addHaar_smul, image_add_left, measure_preimage_add, abs_pow,
        singleton_add]

Premises used: div_eq_mul_inv, Set.image_add_left, Set.singleton_add, MeasureTheory.measure_preimage_add, abs_pow, MeasureTheory.Measure.addHaar_smul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
hb : ENNReal.ofReal (|r| ^ finrank ℝ E) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (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∞)

Tactic:
rw [ENNReal.mul_inv]

Premises used: ENNReal.mul_inv
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne, true_or]

Premises used: not_le, Iff.mpr, pow_pos, ENNReal.ofReal_eq_zero, true_or, Ne, abs_pos
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [ENNReal.ofReal_ne_top, true_or, Ne, not_false_iff]

Premises used: true_or, Ne, ENNReal.ofReal_ne_top, not_false_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
ht : ENNReal.ofReal (|r| ^ finrank ℝ 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∞)

Tactic:
rw [ENNReal.mul_inv_cancel, one_mul, div_eq_mul_inv]

Premises used: div_eq_mul_inv, ENNReal.mul_inv_cancel, one_mul
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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) ≠ 0

Tactic:
simp only [pow_pos (abs_pos.mpr hr), ENNReal.ofReal_eq_zero, not_le, Ne]

Premises used: not_le, Iff.mpr, pow_pos, ENNReal.ofReal_eq_zero, Ne, abs_pos
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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) ≠ ∞

Tactic:
simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]

Premises used: Ne, ENNReal.ofReal_ne_top, not_false_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 μ

Tactic:
⟨⟨(2 : ℝ≥0) ^ finrank ℝ E, ?_⟩⟩

Premises used: Real, IsUnifLocDoublingMeasure.mk, HPow.hPow, Exists.intro, OfNat.ofNat, Module.finrank
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
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∞)
⊢ IsUnifLocDoublingMeasure μ

Tactic:
refine ⟨⟨(2 : ℝ≥0) ^ finrank ℝ E, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
h :
  ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (Ioi 0) r) (x : E),
    (μ : (a : Set E) → ℝ≥0∞) (closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ) 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:
filter_upwards [self_mem_nhdsWithin] with r hr x

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
x : E
h :
  HMul.hMul (β := ℝ≥0∞) (↑(Real.toNNReal 2 ^ finrank ℝ E) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x (2 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
rw [addHaar_closedBall_mul μ x zero_le_two (le_of_lt hr), addHaar_closedBall_center μ x,
    ENNReal.ofReal, Real.toNNReal_pow zero_le_two]

Premises used: Real.toNNReal_pow, ENNReal.ofReal, le_of_lt, zero_le_two, MeasureTheory.Measure.addHaar_closedBall_mul, MeasureTheory.Measure.addHaar_closedBall_center
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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 : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
x : E
⊢ HMul.hMul (β := ℝ≥0∞) (↑(Real.toNNReal 2 ^ finrank ℝ E) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)

Tactic:
simp only [Real.toNNReal_ofNat, le_refl]

Premises used: le_refl, Real.toNNReal_ofNat
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
⊢ FiniteDimensional ℝ G

Tactic:
have : FiniteDimensional ℝ G := b.finiteDimensional_of_finite
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
rw :
  parallelepiped v =
    parallelepiped.{u_2, u_3} (ι := ι)
      (Function.comp (β := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (⇑b : (a : ι) → G))
⊢ parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))

Tactic:
rw [image_parallelepiped]

Premises used: image_parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v =
    parallelepiped.{u_2, u_3} (ι := ι)
      (Function.comp (β := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (⇑b : (a : ι) → G))

Tactic:
congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm

Premises used: congr_arg, funext, Nat, Module.Basis.constr_basis, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v =
    parallelepiped.{u_2, u_3} (ι := ι)
      (Function.comp (β := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (⇑b : (a : ι) → G))

Tactic:
exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm

Premises used: congr_arg, funext, Nat, Module.Basis.constr_basis, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))

Tactic:
have A : parallelepiped v = b.constr ℕ v '' parallelepiped b := by
    rw [image_parallelepiped]
    exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm