awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₁ :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
      (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₂ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| * 1 =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₃ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₄ :
  ENNReal.ofReal
      |Matrix.det.{0, u_2} (n := ι)
          ((LinearMap.toMatrix b b : (a : G →ₗ[ℝ] G) → Matrix ι ι ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v))| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₅ : ENNReal.ofReal |(b.toMatrix v).det| = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₆ rw₇ : ENNReal.ofReal |(b.toMatrix v).det| = ENNReal.ofReal |(b.toMatrix v).det|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|

Tactic:
rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]

Premises used: MeasureTheory.Measure.addHaar_image_linearMap, Module.Basis.toMatrix_eq_toMatrix_constr, mul_one, LinearMap.det_toMatrix, Module.Basis.addHaar_self, Module.Basis.det_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
rw :
  ENNReal.ofReal
    |(HSMul.hSMul (α := ℝ) (β := G [⋀^Fin n]→ₗ[ℝ] ℝ)
            ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ)
            (Basis.det (finBasisOfFinrankEq ℝ G ⋯)) :
          (a : Fin n → G) → ℝ)
        v|
| ENNReal.ofReal |(ω : (a : Fin n → G) → ℝ) v|

Tactic:
rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]

Premises used: Module.finBasisOfFinrankEq, Real, AlternatingMap.eq_smul_basis_det, Fact.out
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
conv_rhs :
  ((ω.measure : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) =
    ENNReal.ofReal
      |(HSMul.hSMul (α := ℝ) (β := G [⋀^Fin n]→ₗ[ℝ] ℝ)
              ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ)
              (Basis.det (finBasisOfFinrankEq ℝ G ⋯)) :
            (a : Fin n → G) → ℝ)
          v|
⊢ ((ω.measure : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(ω : (a : Fin n → G) → ℝ) v|

Tactic:
conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]

Premises used: Module.finBasisOfFinrankEq, Real, AlternatingMap.eq_smul_basis_det, Fact.out
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
⊢ ((ω.measure : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) =
    ENNReal.ofReal
      |(HSMul.hSMul (α := ℝ) (β := G [⋀^Fin n]→ₗ[ℝ] ℝ)
              ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ)
              (Basis.det (finBasisOfFinrankEq ℝ G ⋯)) :
            (a : Fin n → G) → ℝ)
          v|

Tactic:
simp only [addHaar_parallelepiped, AlternatingMap.measure, coe_nnreal_smul_apply,
    AlternatingMap.smul_apply, smul_eq_mul, abs_mul, ENNReal.ofReal_mul (abs_nonneg _),
    ← Real.enorm_eq_ofReal_abs, enorm]

Premises used: MeasureTheory.Measure.coe_nnreal_smul_apply, AlternatingMap.smul_apply, ENNReal.ofReal_mul, abs_mul, MeasureTheory.Measure.addHaar_parallelepiped, Real.enorm_eq_ofReal_abs, ENorm.enorm, smul_eq_mul, abs_nonneg, AlternatingMap.measure
-- 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
ι : Type u_2
G : Type u_3
inst_6 : Fintype ι
inst_7 : DecidableEq ι
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : MeasurableSpace G
inst_11 : BorelSpace G
inst_12 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
rw :
  (HSMul.hSMul (β := Measure G)
      (nnnorm (E := ℝ) ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ))
      (Basis.addHaar (ι := Fin n) (finBasisOfFinrankEq ℝ G ⋯))).IsAddLeftInvariant
⊢ IsAddLeftInvariant ω.measure

Tactic:
rw [AlternatingMap.measure]

Premises used: AlternatingMap.measure
-- 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
ι : Type u_2
G : Type u_3
inst_6 : Fintype ι
inst_7 : DecidableEq ι
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : MeasurableSpace G
inst_11 : BorelSpace G
inst_12 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
⊢ (HSMul.hSMul (β := Measure G)
      (nnnorm (E := ℝ) ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ))
      (Basis.addHaar (ι := Fin n) (finBasisOfFinrankEq ℝ G ⋯))).IsAddLeftInvariant

Tactic:
infer_instance
-- 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
ι : Type u_2
G : Type u_3
inst_6 : Fintype ι
inst_7 : DecidableEq ι
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : MeasurableSpace G
inst_11 : BorelSpace G
inst_12 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
rw :
  IsLocallyFiniteMeasure
    (HSMul.hSMul (β := Measure G)
      (nnnorm (E := ℝ) ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ))
      (Basis.addHaar (ι := Fin n) (finBasisOfFinrankEq ℝ G ⋯)))
⊢ IsLocallyFiniteMeasure (m0 := inst_10) ω.measure

Tactic:
rw [AlternatingMap.measure]

Premises used: AlternatingMap.measure
-- 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
ι : Type u_2
G : Type u_3
inst_6 : Fintype ι
inst_7 : DecidableEq ι
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : MeasurableSpace G
inst_11 : BorelSpace G
inst_12 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
⊢ IsLocallyFiniteMeasure
    (HSMul.hSMul (β := Measure G)
      (nnnorm (E := ℝ) ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G ⋯) : (a : Fin n) → G) : ℝ))
      (Basis.addHaar (ι := Fin n) (finBasisOfFinrankEq ℝ G ⋯)))

Tactic:
infer_instance
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
tendsto_of_tendsto_of_tendsto_of_le_of_le' :
  ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞) ≤
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x b) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)

Tactic:
apply
      tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h
        (Eventually.of_forall fun b => zero_le)

Premises used: zero_le, tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞) ≤
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x a) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞) ≤
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x b) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin]

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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
r : ℝ
rpos : 0 < r
h₁ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
grw [t_bound]
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
r : ℝ
rpos : 0 < r
h₁ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (s ∩ HVAdd.hVAdd (α := Set E) {x} (HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
h₂ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (s ∩ (x +ᵥ HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
h₃ h₄ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
rw [← vadd_eq_add, singleton_vadd, affinity_unitClosedBall rpos.le]

Premises used: affinity_unitClosedBall, LT.lt.le, Set.singleton_vadd, vadd_eq_add
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)

Tactic:
have A : Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0) := by
    apply
      tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h
        (Eventually.of_forall fun b => zero_le)
    filter_upwards [self_mem_nhdsWithin]
    rintro r (rpos : 0 < r)
    grw [t_bound]
    rw [← vadd_eq_add, singleton_vadd, affinity_unitClosedBall rpos.le]
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
apply :
  EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (x_1 : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞))
    fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)
⊢ Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞)))

Tactic:
apply tendsto_const_nhds.congr' _

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞) =
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • u) : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (x_1 : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞))
    fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin]

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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
⊢ closedBall x r = {x} + HSMul.hSMul (β := Set E) r (closedBall 0 1)

Tactic:
simp only [_root_.smul_closedBall, Real.norm_of_nonneg rpos.le, zero_le_one, add_zero,
        mul_one, singleton_add_closedBall, smul_zero]

Premises used: smul_zero, LT.lt.le, zero_le_one, mul_one, add_zero, smul_closedBall, singleton_add_closedBall, Real.norm_of_nonneg
-- 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
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
⊢ closedBall x r = {x} + HSMul.hSMul (β := Set E) r (closedBall 0 1)

Tactic:
have : closedBall x r = {x} + r • closedBall (0 : E) 1 := by
      simp only [_root_.smul_closedBall, Real.norm_of_nonneg rpos.le, zero_le_one, add_zero,
        mul_one, singleton_add_closedBall, smul_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
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
this : closedBall x r = {x} + HSMul.hSMul (β := Set E) r (closedBall 0 1)
h₁ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • u) : ℝ≥0∞)

Tactic:
simp only [this, addHaar_singleton_add_smul_div_singleton_add_smul μ rpos.ne']

Premises used: LT.lt.ne', MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_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
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
this : closedBall x r = {x} + HSMul.hSMul (β := Set E) r (closedBall 0 1)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x 1) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + u) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [addHaar_closedBall_center, image_add_left, measure_preimage_add, singleton_add]

Premises used: Set.image_add_left, Set.singleton_add, MeasureTheory.Measure.addHaar_closedBall_center, MeasureTheory.measure_preimage_add