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

Tactic:
refine liminf_le_liminf ?_ ?_

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

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
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) atTop fun n => ∑ i : γ n, diam (t n i) ^ ↑(Fintype.card ι)

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

Tactic:
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_simp [npos.ne']

Result:
no goals

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

Tactic:
calc
  x i = (a i : ℝ) + (x i - a i) * n / n := by field_simp [npos.ne']
  _ ≤ (a i : ℝ) + (⌊(x i - a i) * n⌋₊ + 1) / n := by
    gcongr
    exact (Nat.lt_floor_add_one _).le

Result:
no goals

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 : ι
⊢ x i = ↑(a i) + (x i - ↑(a i)) * ↑n / ↑n

Tactic:
field_simp [npos.ne']

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), 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)

Tactic:
apply le_antisymm _

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

ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), 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 ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
s : Set (ι → ℝ)
x✝ : diam s ≤ ⊤
⊢ volume s ≤ diam s ^ ↑(Fintype.card ι)

Tactic:
rw [ENNReal.rpow_natCast]

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
s : Set (ι → ℝ)
x✝ : diam s ≤ ⊤
⊢ volume s ≤ diam s ^ Fintype.card ι

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

Tactic:
replace H := fun i => (H i).1

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), 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 ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
⊢ volume ≤ μH[↑(Fintype.card ι)]

Tactic:
refine le_hausdorffMeasure _ _ ∞ ENNReal.coe_lt_top fun s _ => ?_

Result:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
s : Set (ι → ℝ)
x✝ : diam s ≤ ⊤
⊢ volume s ≤ diam s ^ ↑(Fintype.card ι)

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
a✝ : ℕ
hn : ∀ (i : γ a✝), diam (t a✝ i) ≤ 1 / ↑a✝
i : γ a✝
x✝ : i ∈ Finset.univ
⊢ diam (t a✝ i) ^ Fintype.card ι ≤ (1 / ↑a✝) ^ Fintype.card ι

Tactic:
exact pow_le_pow_left' (hn i) _

Result:
no goals

Proof state:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
i : ι
⊢ 0 ≤ ↑(b i) - ↑(a i)

Tactic:
simpa only [sub_nonneg, Rat.cast_le] using (H i).le

Result:
no goals

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)
⊢ Tendsto (fun n => 1 / ↑n) atTop (𝓝 0)

Tactic:
simp only [one_div, ENNReal.tendsto_inv_nat_nhds_zero]

Result:
no goals