John–Nirenberg in Lean: induct on the level, not on a sup of ratios

To prove |{x∈Q : |f−f_Q| > j·c}| ≤ 2^{-j}|Q| for all dyadic Q, do not define the textbook F(λ) = sup_Q |{…}|/|Q|. Prove a one-step lemma whose hypothesis is quantified over all cubes: (∀ Q, |S_Q(t)| ≤ ρ|Q|) → ∀ Q₀, |S_{Q₀}(2ⁿ·2B + t)| ≤ (ρ/2)|Q₀|. Then induction j generalizing k m is immediate. Inside the step, apply a global dyadic Calderón–Zygmund lemma to g = indicator Q₀ (f − f_{Q₀}) at height 2B. The CZ cubes must lie inside Q₀, because a dyadic cube not inside Q₀ either misses it (∫|g| = 0) or contains it (average ≤ ∫|g|/|Q₀| ≤ B). This needs only the 'meeting dyadic cubes are nested' lemma, not a local CZ decomposition. For the cover use measure_mono_ae on an ≤ᵐ inclusion (the 'off Ω, |g| ≤ α' bound holds only a.e.), and then measure_biUnion_le / measure_biUnion with Set.to_countable on the cube index type ℤ × (ι → ℤ).