-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_4
inst : Fintype ι
a b : (i : ι) → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ)
γ : (n : ℕ) → Type u_4 := fun (n : ℕ) ↦ (i : ι) → Fin ⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) :=
  fun (n : ℕ) (f : γ n) ↦
    Set.pi (α := fun (a : ι) ↦ ℝ) Set.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 : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) (⋃ (i : γ n), t n i)
univ :
  LE.le (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HPow.hPow (β := ℝ) (ediam (t n i)) (↑(Fintype.card ι) : ℝ)) atTop)
    (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ^ Fintype.card ι) atTop)
⊢ LE.le (α := ℝ≥0∞)
    (((μH[(↑(Fintype.card ι) : ℝ)] : Measure (ι → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Ioo (↑(a i) : ℝ) (↑(b i) : ℝ)) :
      ℝ≥0∞)
    (∏ x : ι, (volume : (a : Set ℝ) → ℝ≥0∞) ((fun (i : ι) ↦ (Ioo (↑(a i) : ℝ) (↑(b i) : ℝ) : Set ℝ)) x) : ℝ≥0∞)
have univ₁ : Eq (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ∑ i : γ n, HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ^ Fintype.card ι) atTop)
  (liminf
    (fun (n : ℕ) ↦
      ∏ i : ι, HDiv.hDiv (α := ℝ≥0∞) (↑⌈HSub.hSub (α := ℝ) (↑(b i) : ℝ) (↑(a i) : ℝ) * (↑n : ℝ)⌉₊ : ℝ≥0∞) (↑n : ℝ≥0∞))
    atTop)
Tactic: 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]