-- Mathlib/MeasureTheory/Order/UpperLower.lean
/-- If we can fit a small ball inside a set `sᶜ` intersected with any neighborhood of `x`, then the
density of `s` near `x` is not `1`.

Along with `aux₀`, this proves that `x` is a Lebesgue point of `s`. This will be used to prove that
the frontier of an order-connected set is null. -/
private lemma aux₁
    (h : ∀ δ, 0 < δ →
      ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior sᶜ) :
    ¬Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0)
        (𝓝 1)

Proof state:
case intro.intro.intro.refine_1
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) ≠ 0

case intro.intro.intro.refine_2
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ ((fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) ∘ ε) n ≤
    1 - ENNReal.ofReal (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]

Result:
case intro.intro.intro.refine_1
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ ENNReal.ofReal (4⁻¹ ^ Fintype.card ι) ≠ 0

case intro.intro.intro.refine_2
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ε n ≠ 0

case intro.intro.intro.refine_2
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 < (2 * ε n) ^ Fintype.card ι

ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0

ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 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

case intro.intro.intro.refine_2.hr
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n / 4

case intro.intro.intro.refine_2.hr
ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n

ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume

ι : 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 (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 ≤ ε n / 4