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
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 ι)
simp_rw₉ :
  HPow.hPow (α := ENNReal) (↑n : ENNReal)⁻¹ (Finset.card.{u_1} (α := ι) Finset.univ) =
    (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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ Set.Finite.{u_1} (α := ι → ℤ) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s}
have refine_1 : ∀ (ν : ι → ℤ), NullMeasurableSet.{u_1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) ν) volume
Tactic: refine (Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι)
    (by simp) (As := fun ν : ι → ℤ ↦ (box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
      (fun _ hν ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
refine_1 :
  ∀ (ν : ι → ℤ), NullMeasurableSet.{u_1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) ν) volume
⊢ Set.Finite.{u_1} (α := ι → ℤ) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s}
have refine_2 : ∀ (x x_1 : ι → ℤ) (h : x ≠ x_1),
  Function.onFun (β := Set (ι → ℝ)) (AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume)
    (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) x x_1
Tactic: refine (Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι)
    (by simp) (As := fun ν : ι → ℤ ↦ (box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
      (fun _ hν ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
refine_1 :
  ∀ (ν : ι → ℤ), NullMeasurableSet.{u_1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) ν) volume
refine_2 :
  ∀ (x x_1 : ι → ℤ) (h : x ≠ x_1),
    Function.onFun (β := Set (ι → ℝ)) (AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume)
      (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) x x_1
⊢ Set.Finite.{u_1} (α := ι → ℤ) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s}
have refine_3 : Ne (α := ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (⋃ (i : ι → ℤ), (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) i) :
    ENNReal)
  (⊤ : ENNReal)
Tactic: refine (Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι)
    (by simp) (As := fun ν : ι → ℤ ↦ (box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
      (fun _ hν ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
refine_1 :
  ∀ (ν : ι → ℤ), NullMeasurableSet.{u_1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) ν) volume
refine_2 :
  ∀ (x x_1 : ι → ℤ) (h : x ≠ x_1),
    Function.onFun (β := Set (ι → ℝ)) (AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume)
      (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) x x_1
refine_3 :
  Ne (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (⋃ (i : ι → ℤ), (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) i) :
      ENNReal)
    (⊤ : ENNReal)
⊢ Set.Finite.{u_1} (α := ι → ℤ) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s}
have refine_4 : ∀ (x : ι → ℤ) (hν : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s} x),
  Membership.mem (γ := Set (ι → ℤ))
    {i : ι → ℤ |
      1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
        ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n i) : Set (ι → ℝ)) ∩ s)}
    x
Tactic: refine (Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι)
    (by simp) (As := fun ν : ι → ℤ ↦ (box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
      (fun _ hν ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
ν : ι → ℤ
⊢ NullMeasurableSet.{u_1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) ν) volume
have refine_1 : NullMeasurableSet (↑(box n ν) : Set (ι → ℝ)) volume
Tactic: refine NullMeasurableSet.inter ?_ hs₁
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
x : ι → ℤ
hν : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s} x
⊢ Membership.mem (γ := Set (ι → ℤ))
    {i : ι → ℤ |
      1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
        ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n i) : Set (ι → ℝ)) ∩ s)}
    x
have refine_4 : 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n x) : Set (ι → ℝ)) ∩ s)
Tactic: rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
x : ι → ℤ
hν : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s} x
refine_4 :
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n x) : Set (ι → ℝ)) ∩ s)
⊢ Membership.mem (γ := Set (ι → ℤ))
    {i : ι → ℤ |
      1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
        ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n i) : Set (ι → ℝ)) ∩ s)}
    x
have refine_4₁ : 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n x) : Set (ι → ℝ))
Tactic: rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s (volume : Measure (ι → ℝ))
hs₂ : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) (⊤ : ENNReal)
x : ι → ℤ
hν : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s} x
refine_4 :
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n x) : Set (ι → ℝ)) ∩ s)
refine_4₁ :
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑(box n x) : Set (ι → ℝ))
⊢ Membership.mem (γ := Set (ι → ℤ))
    {i : ι → ℤ |
      1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
        ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n i) : Set (ι → ℝ)) ∩ s)}
    x
have refine_4₂ : 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤ 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
Tactic: rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
⊢ Finset (ι → ℤ)
have refine : Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑B : Set (ι → ℝ)) : ENNReal)
  (⊤ : ENNReal)
Tactic: refine (setFinite_index n B.measurableSet_coe.nullMeasurableSet ?_).toFinset
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
⊢ ν ∈ admissibleIndex n B ↔ box n ν ≤ B
have rw : ν ∈ Set.Finite.toFinset (s := {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))}) sorry ↔ box n ν ≤ B
Tactic: rw [admissibleIndex, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Box.coe_subset_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
rw : ν ∈ Set.Finite.toFinset (s := {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))}) ⋯ ↔ box n ν ≤ B
⊢ ν ∈ admissibleIndex n B ↔ box n ν ≤ B
have rw₁ : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))} ν ↔ box n ν ≤ B
Tactic: rw [admissibleIndex, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Box.coe_subset_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
rw : ν ∈ Set.Finite.toFinset (s := {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))}) ⋯ ↔ box n ν ≤ B
rw₁ : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))} ν ↔ box n ν ≤ B
⊢ ν ∈ admissibleIndex n B ↔ box n ν ≤ B
have rw₂ : (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ)) ↔ box n ν ≤ B
Tactic: rw [admissibleIndex, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Box.coe_subset_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
rw : ν ∈ Set.Finite.toFinset (s := {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))}) ⋯ ↔ box n ν ≤ B
rw₁ : Membership.mem (γ := Set (ι → ℤ)) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ))} ν ↔ box n ν ≤ B
rw₂ : (↑(box n ν) : Set (ι → ℝ)) ⊆ (↑B : Set (ι → ℝ)) ↔ box n ν ≤ B
⊢ ν ∈ admissibleIndex n B ↔ box n ν ≤ B
have rw₃ : box n ν ≤ B ↔ box n ν ≤ B
Tactic: rw [admissibleIndex, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Box.coe_subset_coe]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B x : Box ι
hI : Membership.mem (γ := Finset (Box ι)) (Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) x
⊢ x ≤ B
have obtain : ∀ (w : ι → ℤ) (hν : w ∈ admissibleIndex n B)
  (hI :
    Membership.mem (γ := Finset (Box ι)) (Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) (box n w)),
  box n w ≤ B
Tactic: obtain ⟨_, hν, rfl⟩ := Finset.mem_image.mp hI
Cleared hypotheses: x, hI
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B x : Box ι
hI₁ : x ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι))
x_1 : Box ι
hI₂ : x_1 ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι))
h : x ≠ x_1
⊢ Function.onFun Disjoint Box.toSet x x_1
have obtain : ∀ w ∈ admissibleIndex n B,
  ∀ (hI₁ : box n w ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι)))
    (h : box n w ≠ x_1), Function.onFun Disjoint Box.toSet (box n w) x_1
Tactic: obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₁
Cleared hypotheses: x, hI₁, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B x : Box ι
hI₂ : x ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι))
w : ι → ℤ
left : w ∈ admissibleIndex n B
hI₁ : box n w ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι))
h : box n w ≠ x
⊢ Function.onFun Disjoint Box.toSet (box n w) x
have obtain : ∀ w_1 ∈ admissibleIndex n B,
  ∀ (hI₂ : box n w_1 ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι)))
    (h : box n w ≠ box n w_1), Function.onFun Disjoint Box.toSet (box n w) (box n w_1)
Tactic: obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₂
Cleared hypotheses: x, hI₂, h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
      tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
    else ⋯.choose (p := Membership.mem B))
have pos : ∀ (hI : ∃ ν ∈ admissibleIndex n B, I = box n ν),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
      tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
    else sorry.choose (p := Membership.mem B))
Tactic: by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
pos :
  ∀ (hI : ∃ ν ∈ admissibleIndex n B, I = box n ν),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
      (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
        tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
      else ⋯.choose (p := Membership.mem B))
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
      tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
    else ⋯.choose (p := Membership.mem B))
have neg : ∀ (hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
      tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
    else sorry.choose (p := Membership.mem B))
Tactic: by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
      tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
    else ⋯.choose (p := Membership.mem B))
have pos : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
  (tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν)))
Tactic: simp_rw [dif_pos hI]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
      tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
    else ⋯.choose (p := Membership.mem B))
have neg : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
  (sorry.choose (p := Membership.mem B))
Tactic: simp_rw [dif_neg hI]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw : Membership.mem (γ := TaggedPrepartition B)
    { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := sorry, pairwiseDisjoint := sorry,
      tag := fun (I : Box ι) ↦
        if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
          tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
        else sorry.choose (p := Membership.mem B),
      tag_mem_Icc := sorry }
    I ↔
  ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
rw :
  Membership.mem (γ := TaggedPrepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun (I : Box ι) ↦
          if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
            tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
          else ⋯.choose (p := Membership.mem B),
        tag_mem_Icc := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw₁ : Membership.mem (γ := Prepartition B)
    { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := sorry, pairwiseDisjoint := sorry }
    I ↔
  ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
rw :
  Membership.mem (γ := TaggedPrepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun (I : Box ι) ↦
          if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
            tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
          else ⋯.choose (p := Membership.mem B),
        tag_mem_Icc := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
rw₁ :
  Membership.mem (γ := Prepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯,
        pairwiseDisjoint := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw₂ : Membership.mem (γ := Finset (Box ι)) (Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) I ↔
  ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
rw :
  Membership.mem (γ := TaggedPrepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun (I : Box ι) ↦
          if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
            tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
          else ⋯.choose (p := Membership.mem B),
        tag_mem_Icc := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
rw₁ :
  Membership.mem (γ := Prepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯,
        pairwiseDisjoint := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
rw₂ :
  Membership.mem (γ := Finset (Box ι)) (Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw₃ : (∃ a ∈ admissibleIndex n B, box n a = I) ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw : Membership.mem (γ := TaggedPrepartition B)
    { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := sorry, pairwiseDisjoint := sorry,
      tag := fun (I : Box ι) ↦
        if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
          tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
        else sorry.choose (p := Membership.mem B),
      tag_mem_Icc := sorry }
    I ↔
  ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: classical
  rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
rw :
  Membership.mem (γ := TaggedPrepartition B)
      { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
        tag := fun (I : Box ι) ↦
          if hI : ∃ ν ∈ admissibleIndex n B, I = box n ν then
            tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν))
          else ⋯.choose (p := Membership.mem B),
        tag_mem_Icc := ⋯ }
      I ↔
    ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
have rw₁ : Membership.mem (γ := Prepartition B)
    { boxes := Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B), le_of_mem' := sorry, pairwiseDisjoint := sorry }
    I ↔
  ∃ ν ∈ admissibleIndex n B, box n ν = I
Tactic: classical
  rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]