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
s : Set E
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
have I : ∀ (u v : Set E),
  Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
      MeasurableSet v →
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
            ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: have I : ∀ u v, μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v →
    μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u := by
    intro u v uzero utop vmeas
    simp_rw [div_eq_mul_inv]
    rw [← ENNReal.sub_mul]; swap
    · simp only [uzero, ENNReal.inv_eq_top, imp_true_iff, Ne, not_false_iff]
    congr 1
    rw [inter_comm _ u, inter_comm _ u, eq_comm]
    exact ENNReal.eq_sub_of_add_eq' utop (measure_inter_add_diff u vmeas)
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
have apply : EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (r : ℝ) ↦
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: apply tendsto_const_nhds.congr' _
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0) (fun (x : ℝ) ↦ 1) fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) a →
    1 =
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin]
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
⊢ 1 =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 1 =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]
-- 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
s : Set E
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
⊢ 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)
have A : Tendsto (β := ℝ≥0∞)
  (fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
  (𝓝[>] 0) (𝓝 1)
Tactic: have A : Tendsto (fun r => μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1) := by
      apply tendsto_const_nhds.congr' _
      filter_upwards [self_mem_nhdsWithin]
      intro r hr
      rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]
      · exact (measure_closedBall_pos μ _ hr).ne'
      · exact measure_closedBall_lt_top.ne
-- 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
s : Set E
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
⊢ 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)
have B : Tendsto
  (fun (a : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
  (𝓝[>] 0) (𝓝 (HSub.hSub (α := ℝ≥0∞) 1 1))
Tactic: have B := ENNReal.Tendsto.sub A h (Or.inl ENNReal.one_ne_top)
-- 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
s : Set E
hs : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
B :
  Tendsto
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
    (𝓝[>] 0) (𝓝 (HSub.hSub (α := ℝ≥0∞) 1 1))
⊢ 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)
have B₁ : Tendsto (β := ℝ≥0∞)
  (fun (a : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
  (𝓝[>] 0) (𝓝 0)
Tactic: simp only [tsub_self] at B
Cleared hypotheses: B
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
    (𝓝[>] 0) (𝓝 0)
⊢ 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)
have apply : EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
  (fun (a : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
  fun (r : ℝ) ↦
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: apply B.congr' _
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
    (𝓝[>] 0) (𝓝 0)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
    fun (r : ℝ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) a →
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞) =
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (sᶜ ∩ closedBall x a) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin]
-- 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 : MeasurableSet s
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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
I :
  ∀ (u v : Set E),
    Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
        MeasurableSet v →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) -
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (vᶜ ∩ u) : ℝ≥0∞)
                ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) =
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (v ∩ u) : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞)
A :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥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∞))
    (𝓝[>] 0) (𝓝 0)
r : ℝ
rpos : 0 < r
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (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ᶜ ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : s = sᶜᶜ
Tactic: convert!
      I (closedBall x r) sᶜ (measure_closedBall_pos μ _ rpos).ne' measure_closedBall_lt_top.ne
        hs.compl