awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
refine_2 :
  HDiv.hDiv (α := ENNReal) (β := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
          (closedBall x (ε n) \ closedBall (f (ε n) ⋯) (ε n / 4)) :
        ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x (ε n)) : ENNReal) =
    1 - ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι))
⊢ ((fun (r : ℝ) ↦
          HDiv.hDiv (α := ENNReal) (β := ENNReal)
            (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
            (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal)) ∘
        ε)
      n ≤
    1 - ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι))

Tactic:
calc
      volume (closure s ∩ closedBall x (ε n)) / volume (closedBall x (ε n))
        ≤ volume (closedBall x (ε n) \ closedBall (f (ε n) <| hε' n) (ε n / 4)) /
          volume (closedBall x (ε n)) := by
        gcongr
        rw [diff_eq_compl_inter]
        refine inter_subset_inter_left _ ?_
        rw [subset_compl_comm, ← interior_compl]
        exact hf₁ _ _
      _ = 1 - ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) := ?_

Premises used: ENNReal.ofReal, Fintype.card, HDiv.hDiv, Inter.inter, SDiff.sdiff, Inv.inv, closure, HPow.hPow, MeasureTheory.MeasureSpace.volume, Metric.closedBall, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ 0 < ε n

Tactic:
have := hε' n
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
refine_2 : ε n ≠ 0
refine_2₁ : 0 < (2 * ε n) ^ Fintype.card ι
rw : ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0
rw₁ :
  0 < ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) →
    ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) < ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) →
      ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0
refine_2₂ : 0 ≤ ε n / 4
refine_2₃ : 0 ≤ ε n
rw₂ : NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume
rw₃ : 0 ≤ ε n / 4
⊢ HDiv.hDiv (α := ENNReal) (β := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
          (closedBall x (ε n) \ closedBall (f (ε n) ⋯) (ε n / 4)) :
        ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x (ε n)) : ENNReal) =
    1 - ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι))

Tactic:
rw [measure_diff (hf₀ _ _) _ ((Real.volume_pi_closedBall _ _).trans_ne ENNReal.ofReal_ne_top),
      Real.volume_pi_closedBall, Real.volume_pi_closedBall, ENNReal.sub_div fun _ _ ↦ _,
      ENNReal.div_self _ ENNReal.ofReal_ne_top, ← ENNReal.ofReal_div_of_pos, ← div_pow,
      mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div]

Premises used: Real, div_right_comm, ENNReal.ofReal_div_of_pos, two_ne_zero', ENNReal.div_self, ENNReal.sub_div, div_pow, one_div, MeasureTheory.measure_diff, mul_div_mul_left, Eq.trans_ne, ENNReal.ofReal_ne_top, Real.volume_pi_closedBall, div_self
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
refine_2 : ∀ (this : 0 < ε n), ε n ≠ 0
refine_2₁ : ∀ (this : 0 < ε n), 0 < (2 * ε n) ^ Fintype.card ι
on_goal : ∀ (this : 0 < ε n), ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0
on_goal₁ :
  ∀ (this : 0 < ε n),
    0 < ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) →
      ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) < ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) →
        ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0
refine_2₂ : ∀ (this : 0 < ε n), 0 ≤ ε n / 4
refine_2₃ : ∀ (this : 0 < ε n), 0 ≤ ε n
on_goal₂ : ∀ (this : 0 < ε n), NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume
on_goal₃ : ∀ (this : 0 < ε n), 0 ≤ ε n / 4
⊢ ((fun (r : ℝ) ↦
          HDiv.hDiv (α := ENNReal) (β := ENNReal)
            (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
            (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal)) ∘
        ε)
      n ≤
    1 - ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι))

Tactic:
on_goal 2 =>
    calc
      volume (closure s ∩ closedBall x (ε n)) / volume (closedBall x (ε n))
        ≤ volume (closedBall x (ε n) \ closedBall (f (ε n) <| hε' n) (ε n / 4)) /
          volume (closedBall x (ε n)) := by
        gcongr
        rw [diff_eq_compl_inter]
        refine inter_subset_inter_left _ ?_
        rw [subset_compl_comm, ← interior_compl]
        exact hf₁ _ _
      _ = 1 - ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) := ?_
    dsimp only
    have := hε' n
    rw [measure_diff (hf₀ _ _) _ ((Real.volume_pi_closedBall _ _).trans_ne ENNReal.ofReal_ne_top),
      Real.volume_pi_closedBall, Real.volume_pi_closedBall, ENNReal.sub_div fun _ _ ↦ _,
      ENNReal.div_self _ ENNReal.ofReal_ne_top, ← ENNReal.ofReal_div_of_pos, ← div_pow,
      mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div]

Premises used: Real, div_right_comm, ENNReal.ofReal, ENNReal.ofReal_div_of_pos, Fintype.card, HDiv.hDiv, Inter.inter, SDiff.sdiff, two_ne_zero', ENNReal.div_self, ENNReal.sub_div, Inv.inv, closure, HPow.hPow, MeasureTheory.MeasureSpace.volume, div_pow, one_div, MeasureTheory.measure_diff, mul_div_mul_left, Eq.trans_ne, ENNReal.ofReal_ne_top, Metric.closedBall, OfNat.ofNat, DFunLike.coe, Real.volume_pi_closedBall, div_self
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι)) ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι)) ≠ 0

Tactic:
try positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ε n ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ε n ≠ 0

Tactic:
try positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 < (2 * ε n) ^ Fintype.card ι

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 < (2 * ε n) ^ Fintype.card ι

Tactic:
try positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0

Tactic:
try positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n / 4

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n / 4

Tactic:
try positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n

Tactic:
try positivity
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 < ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) →
    ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) < ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) →
      ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume

Tactic:
measurableSet_closedBall.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_closedBall
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume

Tactic:
exact measurableSet_closedBall.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, measurableSet_closedBall
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)

Tactic:
measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)

Premises used: Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, IsClosed.measurableSet, MeasureTheory.measure_mono_null, isClosed_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
refine :
  ∀ (x : ι → ℝ) (hx : x ∈ frontier s),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
          (fun (x : ι → ℝ) ↦
              Tendsto (β := ENNReal)
                (fun (r : ℝ) ↦
                  HDiv.hDiv (α := ENNReal) (β := ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
                (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
            x}ᶜ
      x
⊢ Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)

Tactic:
refine measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)

Premises used: Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, IsClosed.measurableSet, MeasureTheory.measure_mono_null, isClosed_closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
pos :
  ∀ (h : x ∈ closure s),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
          (fun (x : ι → ℝ) ↦
              Tendsto (β := ENNReal)
                (fun (r : ℝ) ↦
                  HDiv.hDiv (α := ENNReal) (β := ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
                (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
            x}ᶜ
      x
neg :
  ∀ (h : x ∉ closure s),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
          (fun (x : ι → ℝ) ↦
              Tendsto (β := ENNReal)
                (fun (r : ℝ) ↦
                  HDiv.hDiv (α := ENNReal) (β := ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
                (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
            x}ᶜ
      x
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x

Tactic:
by_cases h : x ∈ closure s

Premises used: closure
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
pos :
  ¬Tendsto (β := ENNReal)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
      (𝓝[>] 0) (𝓝 1)
⊢ Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
        (fun (x : ι → ℝ) ↦
            Tendsto (β := ENNReal)
              (fun (r : ℝ) ↦
                HDiv.hDiv (α := ENNReal) (β := ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
                  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
              (𝓝[>] 0) (𝓝 ((closure s).indicator 1 x)))
          x}ᶜ
    x

Tactic:
simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]

Premises used: Pi.one_apply, Set.mem_setOf, Set.indicator_of_mem, Set.indicator_of_notMem, not_false_eq_true, Set.mem_compl_iff