awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
simp_rw :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
simp_rw₁ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), index n x x_1 = ν x_1
simp_rw₂ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ - 1 = ν x_1
simp_rw₃ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ = ν x_1 + 1
simp_rw₄ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), HSub.hSub (α := ℝ) (↑(ν x_1 + 1) : ℝ) 1 < (↑n : ℝ) * x x_1 ∧ (↑n : ℝ) * x x_1 ≤ (↑(ν x_1 + 1) : ℝ)
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw₅ : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
  ∀ (x_1 : ι),
    HAdd.hAdd (α := ℝ) (↑(ν x_1) : ℝ) (↑1 : ℝ) - 1 < (↑n : ℝ) * x x_1 ∧
      (↑n : ℝ) * x x_1 ≤ HAdd.hAdd (α := ℝ) (↑(ν x_1) : ℝ) (↑1 : ℝ)
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x : ι → ℝ
ν : ι → ℤ
simp_rw :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔ index n x = ν
simp_rw₁ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), index n x x_1 = ν x_1
simp_rw₂ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ - 1 = ν x_1
simp_rw₃ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), ⌈(↑n : ℝ) * x x_1⌉ = ν x_1 + 1
simp_rw₄ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι), HSub.hSub (α := ℝ) (↑(ν x_1 + 1) : ℝ) 1 < (↑n : ℝ) * x x_1 ∧ (↑n : ℝ) * x x_1 ≤ (↑(ν x_1 + 1) : ℝ)
simp_rw₅ :
  (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
    ∀ (x_1 : ι),
      HAdd.hAdd (α := ℝ) (↑(ν x_1) : ℝ) (↑1 : ℝ) - 1 < (↑n : ℝ) * x x_1 ∧
        (↑n : ℝ) * x x_1 ≤ HAdd.hAdd (α := ℝ) (↑(ν x_1) : ℝ) (↑1 : ℝ)
⊢ x ∈ box n ν ↔ index n x = ν
have simp_rw₆ : (∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1) ↔
  ∀ (x_1 : ι),
    HAdd.hAdd (α := ℝ) (↑(ν x_1) : ℝ) 1 - 1 < (↑n : ℝ) * x x_1 ∧ (↑n : ℝ) * x x_1 ≤ HAdd.hAdd (α := ℝ) (↑(ν x_1) : ℝ) 1
Tactic: simp_rw [mem_box_iff', funext_iff, index_apply, sub_eq_iff_eq_add, Int.ceil_eq_iff,
    Int.cast_add, Int.cast_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
⊢ ν ≠ ν' ↔ Disjoint (↑(box n ν) : Set (ι → ℝ)) (↑(box n ν') : Set (ι → ℝ))
have rw : (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) ↔ ν = ν'
Tactic: rw [not_iff_comm, Set.not_disjoint_iff]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
⊢ (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) ↔ ν = ν'
have refine : (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) →
  ∀ (x : ι → ℝ) (hx : x ∈ (↑(box n ν) : Set (ι → ℝ))) (hx' : x ∈ (↑(box n ν') : Set (ι → ℝ))), ν = ν'
Tactic: refine ⟨fun ⟨x, hx, hx'⟩ ↦ ?_, fun h ↦ ⟨tag n ν, tag_mem n ν, h ▸ tag_mem n ν⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
h : ∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))
x : ι → ℝ
hx : x ∈ (↑(box n ν) : Set (ι → ℝ))
hx' : x ∈ (↑(box n ν') : Set (ι → ℝ))
⊢ ν = ν'
have rw : index n x = ν'
Tactic: rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
h : ∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))
x : ι → ℝ
hx : x ∈ (↑(box n ν) : Set (ι → ℝ))
hx' : x ∈ (↑(box n ν') : Set (ι → ℝ))
rw : index n x = ν'
⊢ ν = ν'
have rw₁ : index n x = index n x
Tactic: rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
a₁ a₂ : ι → ℤ
h : Eq.{u_1 + 1} (α := Box ι) ((fun (ν : ι → ℤ) ↦ box n ν) a₁) ((fun (ν : ι → ℤ) ↦ box n ν) a₂)
⊢ a₁ = a₂
have contrapose! : ∀ (h : a₁ ≠ a₂), box n a₁ ≠ box n a₂
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
i : ι
⊢ (box n ν).upper i - (box n ν).lower i = HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have simp_rw : HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ) - HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) = HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: simp_rw [box, add_div, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
i : ι
simp_rw :
  HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ) - HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ (box n ν).upper i - (box n ν).lower i = HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have simp_rw₁ : HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) =
  HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: simp_rw [box, add_div, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
⊢ Metric.diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν)) ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have rw : Metric.diam.{u_1} (α := ι → ℝ)
    (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤
  HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
Tactic: rw [BoxIntegral.Box.Icc_eq_pi]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
⊢ Metric.diam.{u_1} (α := ι → ℝ)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
have refine : ∀ (i : ι),
  Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: refine ENNReal.toReal_le_of_le_ofReal (by positivity) <| Metric.ediam_pi_le_of_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
i : ι
⊢ Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have simp_rw : ENNReal.ofReal ((box n ν).upper i - (box n ν).lower i) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: simp_rw [Real.ediam_Icc, box.upper_sub_lower, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
i : ι
simp_rw : ENNReal.ofReal ((box n ν).upper i - (box n ν).lower i) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
have simp_rw₁ : ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
Tactic: simp_rw [Real.ediam_Icc, box.upper_sub_lower, le_rfl]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw : ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
    (↑(box n ν) : Set (ι → ℝ)) =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₁ : ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
    (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₂ : ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₃ : ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₃ :
  ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₄ : ∏ x : ι, ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₃ :
  ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₄ :
  ∏ x : ι, ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₅ : ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₃ :
  ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₄ :
  ∏ x : ι, ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₅ :
  ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₆ : (ENNReal.ofReal 1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₃ :
  ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₄ :
  ∏ x : ι, ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₅ :
  ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₆ :
  (ENNReal.ofReal 1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₇ : (1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₃ :
  ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₄ :
  ∏ x : ι, ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₅ :
  ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₆ :
  (ENNReal.ofReal 1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₇ :
  (1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₈ : HDiv.hDiv (α := ENNReal) 1 (↑n : ENNReal) ^ Finset.card.{u_1} (α := ι) Finset.univ =
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
simp_rw :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₁ :
  ((Measure.pi (α := fun (i : ι) ↦ ℝ) fun (x : ι) ↦ volume : Measure ((i : ι) → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Set.pi (α := fun (i : ι) ↦ ℝ) Set.univ fun (i : ι) ↦ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₂ :
  ∏ i : ι, (volume : (a : Set ℝ) → ENNReal) (Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₃ :
  ∏ x : ι, ENNReal.ofReal ((box n ν).upper x - (box n ν).lower x) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₄ :
  ∏ x : ι, ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) = 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₅ :
  ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₆ :
  (ENNReal.ofReal 1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₇ :
  (1 / ENNReal.ofReal (↑n : ℝ)) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
simp_rw₈ :
  HDiv.hDiv (α := ENNReal) 1 (↑n : ENNReal) ^ Finset.card.{u_1} (α := ι) Finset.univ =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n ν) : Set (ι → ℝ)) =
    1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
have simp_rw₉ : HPow.hPow (α := ENNReal) (↑n : ENNReal)⁻¹ (Finset.card.{u_1} (α := ι) Finset.univ) =
  (HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι))⁻¹
Tactic: simp_rw [volume_pi, BoxIntegral.Box.coe_eq_pi, Measure.pi_pi, Real.volume_Ioc,
    box.upper_sub_lower, Finset.prod_const, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr
    n.pos_of_neZero), ENNReal.ofReal_one, ENNReal.ofReal_natCast, one_div, ENNReal.inv_pow,
    Finset.card_univ]