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

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

Tactic:
refine ENNReal.tendsto_finset_prod_of_ne_top _ (fun i _ => ?_) fun i _ => ?_

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

case h.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
i : ι
x✝ : i ∈ Finset.univ
⊢ ENNReal.ofReal (↑(b i) - ↑(a 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 : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
⊢ x ∈ ⋃ i, t n i

Tactic:
simp only [t, mem_iUnion, mem_Ioo, mem_univ_pi]

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

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

Tactic:
apply Finset.sum_le_sum fun i _ => _

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 ι

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 : ℕ) in atTop, ∀ (i : γ n), diam (t n i) ≤ 1 / ↑n

Tactic:
refine 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)
n : ℕ
hn : n ≥ 1
⊢ ∀ (i : γ n), diam (t n 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⌉₊
⊢ μH[↑(Fintype.card ι)] (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ≤ ∏ x : ι, volume ((fun i => Ioo ↑(a i) ↑(b i)) x)

Tactic:
let t : ∀ n : ℕ, γ n → Set (ι → ℝ) := fun n f =>
  Set.pi univ fun i => Icc (a i + f i / n) (a i + (f i + 1) / 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⌉₊
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)

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:
exact Real.volume_pi_le_diam_pow s

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
⊢ (univ.pi fun i => Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i

Tactic:
intro x 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 : x ∈ univ.pi fun i => Ioo ↑(a i) ↑(b i)
⊢ x ∈ ⋃ 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)

Tactic:
simpa only [Rat.cast_lt, sub_pos] using H i

Result:
no goals