-- 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)
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, ∀ (i_1 : ι), x i_1 ∈ Icc (↑(a i_1) + ↑↑(i i_1) / ↑n) (↑(a i_1) + (↑↑(i i_1) + 1) / ↑n)

Tactic:
refine ⟨f, fun i => ⟨?_, ?_⟩⟩

Result:
case refine_1
ι : 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) + ↑↑(f i) / ↑n ≤ x i

case refine_2
ι : 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) + (↑↑(f i) + 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
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 = x i

Tactic:
field_simp [npos.ne']

Result:
no goals

Proof state:
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

Tactic:
exact (Nat.lt_floor_add_one _).le

Result:
no goals

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

Tactic:
obtain rfl : s = fun i => Ioo (α := ℝ) (a i) (b i) := funext fun i => (H i).2

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), ∃ (_ : a i < b i), (fun i => Ioo ↑(a i) ↑(b i)) i = Ioo ↑(a i) ↑(b i)
⊢ μ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 ι
s : ι → Set ℝ
hs : ∀ (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)

Tactic:
choose a b H using hs

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

Proof state:
case h.refine_1
ι : 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
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
i : ι
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun n => ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) atTop (𝓝 (ENNReal.ofReal (↑(b i) - ↑(a i))))

Tactic:
apply
  Tendsto.congr' _
    ((ENNReal.continuous_ofReal.tendsto _).comp
      ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))

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
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
i : ι
x✝ : i ∈ Finset.univ
⊢ ENNReal.ofReal ∘ (fun x => ↑⌈(↑(b i) - ↑(a i)) * x⌉₊ / x) ∘ Nat.cast =ᶠ[atTop] fun n =>
    ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑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
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 / ↑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

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
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ liminf (fun n => ∑ i : γ n, (1 / ↑n) ^ Fintype.card ι) atTop =
    liminf (fun n => ∏ i : ι, ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) atTop

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

Result:
no goals