-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_pi_real {ι : Type*} [Fintype ι] :
    (μH[Fintype.card ι] : Measure (ι → ℝ)) = volume

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
n : ℕ
hn : n ≥ 1
f : γ n
⊢ diam (t n f) ≤ 1 / ↑n

Tactic:
refine diam_pi_le_of_le fun b => ?_

Result:
ι : Type u_4
inst✝ : Fintype ι
a b✝ : ι → ℚ
H : ∀ (i : ι), a i < b✝ i
I : ∀ (i : ι), 0 ≤ ↑(b✝ i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b✝ i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
n : ℕ
hn : n ≥ 1
f : γ n
b : ι
⊢ diam (Icc (↑(a b) + ↑↑(f b) / ↑n) (↑(a b) + (↑↑(f b) + 1) / ↑n)) ≤ 1 / ↑n

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
⊢ (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i

Tactic:
have npos : (0 : ℝ) < n := Nat.cast_pos.2 hn

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
⊢ (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i

Proof state:
case h'
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
i : ι
⊢ 0 < (↑(b i) - ↑(a i)) * ↑n

Tactic:
refine mul_pos ?_ npos

Result:
case h'
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
i : ι
⊢ 0 < ↑(b i) - ↑(a i)

Proof state:
ι : Type u_4
inst✝ : Fintype ι
⊢ μH[↑(Fintype.card ι)] = volume

Tactic:
refine (pi_eq_generateFrom (fun _ => Real.borel_eq_generateFrom_Ioo_rat.symm)
  (fun _ => Real.isPiSystem_Ioo_rat) (fun _ => Real.finiteSpanningSetsInIooRat _) ?_).symm

Result:
ι : Type u_4
inst✝ : Fintype ι
⊢ ∀ (s : ι → Set ℝ),
    (∀ (i : ι), s i ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}) → μH[↑(Fintype.card ι)] (univ.pi s) = ∏ i : ι, volume (s i)

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
x : ι → ℝ
hx : x ∈ univ.pi fun i => Ioo ↑(a i) ↑(b i)
⊢ x ∈ ⋃ i, t n i

Tactic:
simp only [mem_Ioo, mem_univ_pi] at hx

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
⊢ x ∈ ⋃ i, t n i

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b✝ : ι → ℚ
H : ∀ (i : ι), a i < b✝ i
I : ∀ (i : ι), 0 ≤ ↑(b✝ i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b✝ i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
n : ℕ
hn : n ≥ 1
f : γ n
b : ι
⊢ diam (Icc (↑(a b) + ↑↑(f b) / ↑n) (↑(a b) + (↑↑(f b) + 1) / ↑n)) ≤ 1 / ↑n

Tactic:
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]

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : Fintype ι
⊢ ∀ (s : ι → Set ℝ),
    (∀ (i : ι), s i ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}) → μH[↑(Fintype.card ι)] (univ.pi s) = ∏ i : ι, volume (s i)

Tactic:
simp only [mem_iUnion, mem_singleton_iff]

Result:
ι : Type u_4
inst✝ : Fintype ι
⊢ ∀ (s : ι → Set ℝ),
    (∀ (i : ι), ∃ i_1 i_2, ∃ (_ : i_1 < i_2), s i = Ioo ↑i_1 ↑i_2) →
      μH[↑(Fintype.card ι)] (univ.pi s) = ∏ x : ι, volume (s x)

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ≤ ∏ x : ι, volume ((fun i => Ioo ↑(a i) ↑(b i)) x)

Tactic:
let γ := fun n : ℕ => ∀ i : ι, Fin ⌈((b i : ℝ) - a i) * n⌉₊

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ≤ ∏ x : ι, volume ((fun i => Ioo ↑(a i) ↑(b i)) x)

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
f : γ n := fun i => ⟨⌊(x i - ↑(a i)) * ↑n⌋₊, ⋯⟩
i : ι
⊢ ↑(a i) + (x i - ↑(a i)) * ↑n / ↑n ≤ ↑(a i) + (↑⌊(x i - ↑(a i)) * ↑n⌋₊ + 1) / ↑n

Tactic:
gcongr

Result:
case bc.hab
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n => (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f => univ.pi fun i => Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n
n : ℕ
hn : n ≥ 1
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
f : γ n := fun i => ⟨⌊(x i - ↑(a i)) * ↑n⌋₊, ⋯⟩
i : ι
⊢ (x i - ↑(a i)) * ↑n ≤ ↑⌊(x i - ↑(a i)) * ↑n⌋₊ + 1