-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_4
inst : Fintype ι
it :
  ∀ (s : (i : ι) → Set ℝ),
    (∀ (i : ι),
        Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) (s i)) →
      Eq (α := ℝ≥0∞)
        (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
            (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
          ℝ≥0∞)
        (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s i) : ℝ≥0∞)
it₁ it₂ :
  ∀ (s : (i : ι) → Set ℝ) (hs : ∀ (i : ι), ∃ (i_1 : ℚ) (i_2 : ℚ) (_ : i_1 < i_2), s i = Ioo (↑i_1 : ℝ) (↑i_2 : ℝ)),
    Eq (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x) : ℝ≥0∞)
it₃ :
  ∀ (s : (i : ι) → Set ℝ) (a b : (i : ι) → ℚ) (H : ∀ (i : ι), ∃ (_ : a i < b i), s i = Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)),
    Eq (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ s) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (s x) : ℝ≥0∞)
it₄ :
  ∀ (a b : (i : ι) → ℚ)
    (H :
      ∀ (i : ι),
        ∃ (_ : a i < b i),
          Eq (α := Set ℝ) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) i) (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ))),
    Eq (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
it₅ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i),
    Eq (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
it₆ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i),
    LE.le (α := ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
        ℝ≥0∞)
it₇ it₈ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i),
    LE.le (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
it₉ it₁₀ it₁₁ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i) (I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)),
    LE.le (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
it₁₂ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i) (I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ))
    (A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0)),
    LE.le (α := ℝ≥0∞)
      (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
        ℝ≥0∞)
      (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
it₁₃ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i) (I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)),
    let γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦
      (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊;
    let t : (n : ℕ) → γ n → Set (ι → ℝ) := fun (n : ℕ) (f : γ n) ↦
      Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
        Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
          ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ));
    ∀ (A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0))
      (B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)),
      LE.le (α := ℝ≥0∞)
        (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
            (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
          ℝ≥0∞)
        (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
it₁₄ :
  ∀ (a b : (i : ι) → ℚ) (H : ∀ (i : ι), a i < b i) (I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)),
    let γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦
      (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊;
    let t : (n : ℕ) → γ n → Set (ι → ℝ) := fun (n : ℕ) (f : γ n) ↦
      Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (i : ι) ↦
        Icc ((↑(a i) : ℝ) + HDiv.hDiv (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) (↑n : ℝ))
          ((↑(a i) : ℝ) + HAdd.hAdd (α := ℝ) (↑(↑(f i) : ℕ) : ℝ) 1 / (↑n : ℝ));
    ∀ (A : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)) atTop (𝓝 0))
      (B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞))
      (C :
        ∀ᶠ (n : ℕ) in atTop,
          Subset.{u_4} (α := Set ((i : ι) → ℝ))
            (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)),
      LE.le (α := ℝ≥0∞)
        (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
            (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
          ℝ≥0∞)
        (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := Measure (ι → ℝ)) (μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))

Tactic:
classical
  -- it suffices to check that the two measures coincide on products of rational intervals
  refine (pi_eq_generateFrom (fun _ => Real.borel_eq_generateFrom_Ioo_rat.symm)
    (fun _ => Real.isPiSystem_Ioo_rat) (fun _ => Real.finiteSpanningSetsInIooRat _) ?_).symm
  simp only [mem_iUnion, mem_singleton_iff]
  -- fix such a product `s` of rational intervals, of the form `Π (a i, b i)`.
  intro s hs
  choose a b H using hs
  obtain rfl : s = fun i => Ioo (α := ℝ) (a i) (b i) := funext fun i => (H i).2
  replace H := fun i => (H i).1
  apply le_antisymm _
  -- first check that `volume s ≤ μH s`
  · have Hle : volume ≤ (μH[Fintype.card ι] : Measure (ι → ℝ)) := by
      refine le_hausdorffMeasure _ _ ∞ ENNReal.coe_lt_top fun s _ => ?_
      rw [ENNReal.rpow_natCast]
      exact Real.volume_pi_le_diam_pow s
    rw [← volume_pi_pi fun i => Ioo (a i : ℝ) (b i)]
    exact Measure.le_iff'.1 Hle _
  /- For the other inequality `μH s ≤ volume s`, we use a covering of `s` by sets of small diameter
    `1/n`, namely cubes with left-most point of the form `a i + f i / n` with `f i` ranging between
    `0` and `⌈(b i - a i) * n⌉`. Their number is asymptotic to `n^d * Π (b i - a i)`. -/
  have I : ∀ i, 0 ≤ (b i : ℝ) - a i := fun i => by
    simpa only [sub_nonneg, Rat.cast_le] using (H i).le
  let γ := fun n : ℕ => ∀ i : ι, Fin ⌈((b i : ℝ) - a i) * n⌉₊
  let t : ∀ n : ℕ, γ n → Set (ι → ℝ) := fun n f =>
    Set.pi univ fun i => Icc (a i + f i / n) (a i + (f i + 1) / n)
  have A : Tendsto (fun n : ℕ => 1 / (n : ℝ≥0∞)) atTop (𝓝 0) := by
    simp only [one_div, ENNReal.tendsto_inv_nat_nhds_zero]
  have B : ∀ᶠ n in atTop, ∀ i : γ n, ediam (t n i) ≤ 1 / n := by
    refine eventually_atTop.2 ⟨1, fun n hn => ?_⟩
    intro f
    refine ediam_pi_le_of_le fun b => ?_
    simp only [Real.ediam_Icc, add_div, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), le_refl,
      add_sub_add_left_eq_sub, add_sub_cancel_left, ENNReal.ofReal_one, ENNReal.ofReal_natCast]
  have C : ∀ᶠ n in atTop, (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ⊆ ⋃ i : γ n, t n i := by
    refine eventually_atTop.2 ⟨1, fun n hn => ?_⟩
    have npos : (0 : ℝ) < n := Nat.cast_pos.2 hn
    intro x hx
    simp only [mem_Ioo, mem_univ_pi] at hx
    simp only [t, mem_iUnion, mem_univ_pi]
    let f : γ n := fun i =>
      ⟨⌊(x i - a i) * n⌋₊, by
        apply Nat.floor_lt_ceil_of_lt_of_pos
        · gcongr
          exact (hx i).right
        · refine mul_pos ?_ npos
          simpa only [Rat.cast_lt, sub_pos] using H i⟩
    refine ⟨f, fun i => ⟨?_, ?_⟩⟩
    · calc
        (a i : ℝ) + ⌊(x i - a i) * n⌋₊ / n ≤ (a i : ℝ) + (x i - a i) * n / n := by
          gcongr
          exact Nat.floor_le (mul_nonneg (sub_nonneg.2 (hx i).1.le) npos.le)
        _ = x i := by field
    · calc
        x i = (a i : ℝ) + (x i - a i) * n / n := by field
        _ ≤ (a i : ℝ) + (⌊(x i - a i) * n⌋₊ + 1) / n := by
          gcongr
          exact (Nat.lt_floor_add_one _).le
  calc
    μH[Fintype.card ι] (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ≤
        liminf (fun n : ℕ => ∑ i : γ n, ediam (t n i) ^ ((Fintype.card ι) : ℝ)) atTop :=
      hausdorffMeasure_le_liminf_sum _ (Set.pi univ fun i => Ioo (a i : ℝ) (b i))
        (fun n : ℕ => 1 / (n : ℝ≥0∞)) A t B C
    _ ≤ liminf (fun n : ℕ => ∑ i : γ n, (1 / (n : ℝ≥0∞)) ^ Fintype.card ι) atTop := by
      refine liminf_le_liminf ?_ ?_
      · filter_upwards [B] with _ hn
        apply Finset.sum_le_sum fun i _ => _
        simp only [ENNReal.rpow_natCast]
        intro i _
        exact pow_le_pow_left' (hn i) _
      · isBoundedDefault
    _ = liminf (fun n : ℕ => ∏ i : ι, (⌈((b i : ℝ) - a i) * n⌉₊ : ℝ≥0∞) / n) atTop := by
      simp only [γ, Finset.card_univ, Nat.cast_prod, one_mul, Fintype.card_fin, Finset.sum_const,
        nsmul_eq_mul, Fintype.card_pi, div_eq_mul_inv, Finset.prod_mul_distrib, Finset.prod_const]
    _ = ∏ i : ι, volume (Ioo (a i : ℝ) (b i)) := by
      simp only [Real.volume_Ioo]
      apply Tendsto.liminf_eq
      refine ENNReal.tendsto_finsetProd_of_ne_top _ (fun i _ => ?_) fun i _ => ?_
      · apply
          Tendsto.congr' _
            ((ENNReal.continuous_ofReal.tendsto _).comp
              ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))
        apply eventually_atTop.2 ⟨1, fun n hn => _⟩
        intro n hn
        simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply,
          ENNReal.ofReal_natCast]
      · simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]

Premises used: Real.borel_eq_generateFrom_Ioo_rat, Set.mem_iUnion, Real.finiteSpanningSetsInIooRat, MeasureTheory.Measure.pi_eq_generateFrom, le_antisymm, Set.mem_singleton_iff, Eq.symm, rfl, Real.isPiSystem_Ioo_rat