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

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
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 ι

Tactic:
filter_upwards [B] with _ hn

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
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✝, diam (t a✝ i) ^ ↑(Fintype.card ι) ≤ ∑ i : γ a✝, (1 / ↑a✝) ^ 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
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

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

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

Tactic:
exact Nat.floor_le (mul_nonneg (sub_nonneg.2 (hx i).1.le) npos.le)

Result:
no goals

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 : ι
⊢ x i - ↑(a i) < ↑(b i) - ↑(a i)

Tactic:
simp only [(hx i).right, sub_lt_sub_iff_right]

Result:
no goals

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

Tactic:
intro s hs

Result:
ι : 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)

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

Tactic:
rw [← volume_pi_pi fun i => Ioo (a i : ℝ) (b i)]

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

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

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

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

Tactic:
have A : Tendsto (fun n : ℕ => 1 / (n : ℝ≥0∞)) atTop (𝓝 0) := by
  simp only [one_div, ENNReal.tendsto_inv_nat_nhds_zero]

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

Tactic:
simp only [ENNReal.rpow_natCast]

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