awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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)
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
⊢ Set.Finite.{u_1} (α := ι → ℤ) {ν : ι → ℤ | (↑(box n ν) : Set (ι → ℝ)) ⊆ s}

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ν ↦ ?_)

Premises used: Set.Finite.subset, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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

Tactic:
NullMeasurableSet.inter ?_ hs₁

Premises used: MeasureTheory.NullMeasurableSet.inter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (↑(box n ν) : Set (ι → ℝ)) volume
⊢ NullMeasurableSet.{u_1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) ν) volume

Tactic:
refine NullMeasurableSet.inter ?_ hs₁

Premises used: MeasureTheory.NullMeasurableSet.inter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (↑(box n ν) : Set (ι → ℝ)) volume

Tactic:
(box n ν).measurableSet_coe.nullMeasurableSet

Premises used: BoxIntegral.Box.measurableSet_coe, MeasurableSet.nullMeasurableSet, BoxIntegral.unitPartition.box
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (↑(box n ν) : Set (ι → ℝ)) volume

Tactic:
exact (box n ν).measurableSet_coe.nullMeasurableSet

Premises used: BoxIntegral.Box.measurableSet_coe, MeasurableSet.nullMeasurableSet, BoxIntegral.unitPartition.box
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 x_1 : ι → ℤ
h : x ≠ x_1
⊢ Function.onFun (β := Set (ι → ℝ)) (AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume)
    (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) x x_1

Tactic:
((Disjoint.inter_right _ (disjoint.mp h)).inter_left _).aedisjoint

Premises used: Disjoint.inter_right, BoxIntegral.unitPartition.disjoint, Disjoint.aedisjoint, Disjoint.inter_left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 x_1 : ι → ℤ
h : x ≠ x_1
⊢ Function.onFun (β := Set (ι → ℝ)) (AEDisjoint (m := MeasureSpace.toMeasurableSpace) volume)
    (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) x x_1

Tactic:
exact ((Disjoint.inter_right _ (disjoint.mp h)).inter_left _).aedisjoint

Premises used: Disjoint.inter_right, BoxIntegral.unitPartition.disjoint, Disjoint.aedisjoint, Disjoint.inter_left, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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)
⊢ ⋃ (i : ι → ℤ), (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) i ⊆ s

Tactic:
simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]

Premises used: Set.iUnion_subset_iff, implies_true, Set.inter_subset_right
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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)
⊢ Ne (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (⋃ (i : ι → ℤ), (fun (ν : ι → ℤ) ↦ (↑(box n ν) : Set (ι → ℝ)) ∩ s) i) :
      ENNReal)
    (⊤ : ENNReal)

Tactic:
exact lt_top_iff_ne_top.mp <| measure_lt_top_of_subset
      (by simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]) hs₂

Premises used: MeasureTheory.measure_lt_top_of_subset, lt_top_iff_ne_top, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (ι → ℝ))
refine_4₂ refine_4₃ :
  1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤ 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)
⊢ Membership.mem (γ := Set (ι → ℤ))
    {i : ι → ℤ |
      1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι) ≤
        ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) ((↑(box n i) : Set (ι → ℝ)) ∩ s)}
    x

Tactic:
rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box]

Premises used: Set.mem_setOf, BoxIntegral.unitPartition.volume_box, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
refine :
  Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑B : Set (ι → ℝ)) : ENNReal)
    (⊤ : ENNReal)
⊢ Finset (ι → ℤ)

Tactic:
refine (setFinite_index n B.measurableSet_coe.nullMeasurableSet ?_).toFinset

Premises used: BoxIntegral.Box.measurableSet_coe, MeasurableSet.nullMeasurableSet, BoxIntegral.unitPartition.setFinite_index, Set.Finite.toFinset
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
⊢ Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑B : Set (ι → ℝ)) : ENNReal)
    (⊤ : ENNReal)

Tactic:
lt_top_iff_ne_top.mp (IsBounded.measure_lt_top B.isBounded)

Premises used: BoxIntegral.Box.isBounded, lt_top_iff_ne_top, Bornology.IsBounded.measure_lt_top, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
⊢ Ne (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (↑B : Set (ι → ℝ)) : ENNReal)
    (⊤ : ENNReal)

Tactic:
exact lt_top_iff_ne_top.mp (IsBounded.measure_lt_top B.isBounded)

Premises used: BoxIntegral.Box.isBounded, lt_top_iff_ne_top, Bornology.IsBounded.measure_lt_top, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
rw₃ rw₄ : box n ν ≤ B ↔ box n ν ≤ B
⊢ ν ∈ admissibleIndex n B ↔ box n ν ≤ B

Tactic:
rw [admissibleIndex, Set.Finite.mem_toFinset, Set.mem_setOf_eq, Box.coe_subset_coe]

Premises used: Set.Finite.mem_toFinset, Set.mem_setOf_eq, BoxIntegral.unitPartition.admissibleIndex, BoxIntegral.Box.coe_subset_coe
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
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
⊢ x ≤ B

Tactic:
obtain ⟨_, hν, rfl⟩ := Finset.mem_image.mp hI

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
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:
mem_admissibleIndex_iff.mp hν

Premises used: BoxIntegral.unitPartition.mem_admissibleIndex_iff, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
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:
exact mem_admissibleIndex_iff.mp hν

Premises used: BoxIntegral.unitPartition.mem_admissibleIndex_iff, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
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
⊢ Function.onFun Disjoint Box.toSet x x_1

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₁

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
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)
⊢ Function.onFun Disjoint Box.toSet (box n w) x

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₂

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
w : ι → ℤ
left : w ∈ admissibleIndex n B
hI₁ : box n w ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι))
w_1 : ι → ℤ
left_1 : 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:
disjoint.mp fun x ↦ h (congrArg (box n) x)

Premises used: congrArg, BoxIntegral.unitPartition.disjoint, Iff.mp, BoxIntegral.unitPartition.box
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
w : ι → ℤ
left : w ∈ admissibleIndex n B
hI₁ : box n w ∈ (↑(Finset.image (fun (ν : ι → ℤ) ↦ box n ν) (admissibleIndex n B)) : Set (Box ι))
w_1 : ι → ℤ
left_1 : 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:
exact disjoint.mp fun x ↦ h (congrArg (box n) x)

Premises used: congrArg, BoxIntegral.unitPartition.disjoint, Iff.mp, BoxIntegral.unitPartition.box
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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))
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 ⋯.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))

Tactic:
by_cases hI : ∃ ν ∈ admissibleIndex n B, I = box n ν

Premises used: BoxIntegral.unitPartition.admissibleIndex
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
hI : ∃ ν ∈ admissibleIndex n B, I = box n ν
pos :
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ 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))

Tactic:
simp_rw [dif_pos hI]

Premises used: dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (ι → ℝ))
    (tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν)))

Tactic:
Box.coe_subset_Icc <| (mem_admissibleIndex_iff.mp hI.choose_spec.1) (tag_mem n _)

Premises used: Exists.choose_spec, BoxIntegral.unitPartition.mem_admissibleIndex_iff, BoxIntegral.unitPartition.tag_mem, And.left, Iff.mp, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (ι → ℝ))
    (tag n (hI.choose (p := fun (ν : ι → ℤ) ↦ ν ∈ admissibleIndex n B ∧ I = box n ν)))

Tactic:
exact Box.coe_subset_Icc <| (mem_admissibleIndex_iff.mp hI.choose_spec.1) (tag_mem n _)

Premises used: Exists.choose_spec, BoxIntegral.unitPartition.mem_admissibleIndex_iff, BoxIntegral.unitPartition.tag_mem, And.left, Iff.mp, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
hI : ¬∃ ν ∈ admissibleIndex n B, I = box n ν
neg :
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ))
    (⋯.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))

Tactic:
simp_rw [dif_neg hI]

Premises used: dif_neg
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (ι → ℝ))
    (⋯.choose (p := Membership.mem B))

Tactic:
Box.coe_subset_Icc B.exists_mem.choose_spec

Premises used: Exists.choose_spec, BoxIntegral.Box.coe_subset_Icc, BoxIntegral.Box.exists_mem
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 (ι → ℝ))
    (⋯.choose (p := Membership.mem B))

Tactic:
exact Box.coe_subset_Icc B.exists_mem.choose_spec

Premises used: Exists.choose_spec, BoxIntegral.Box.coe_subset_Icc, BoxIntegral.Box.exists_mem
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
rw₃ rw₄ : (∃ a ∈ admissibleIndex n B, box n a = I) ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I

Tactic:
rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]

Premises used: Finset.mem_image, BoxIntegral.TaggedPrepartition.mem_mk, BoxIntegral.Prepartition.mem_mk, BoxIntegral.unitPartition.prepartition
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
rw₃ rw₄ : (∃ a ∈ admissibleIndex n B, box n a = I) ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I
⊢ I ∈ prepartition n B ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I

Tactic:
classical
  rw [prepartition, TaggedPrepartition.mem_mk, Prepartition.mem_mk, Finset.mem_image]

Premises used: Finset.mem_image, BoxIntegral.TaggedPrepartition.mem_mk, BoxIntegral.Prepartition.mem_mk, BoxIntegral.unitPartition.prepartition
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
⊢ I ∈ (prepartition n B).boxes ↔ ∃ ν ∈ admissibleIndex n B, box n ν = I

Tactic:
mem_prepartition_iff

Premises used: BoxIntegral.unitPartition.mem_prepartition_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'

Tactic:
have h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν' := ⟨ν, hν, rfl⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
rw : box n (h.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1)) = box n ν
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then
      tag n (hI.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1))
    else ⋯.choose (p := Membership.mem B)) =
    tag n ν

Tactic:
rw [dif_pos h, (tag_injective n).eq_iff, ← (box_injective n).eq_iff]

Premises used: BoxIntegral.unitPartition.tag_injective, BoxIntegral.unitPartition.box_injective, Function.Injective.eq_iff, dif_pos
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ box n (h.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1)) = box n ν

Tactic:
h.choose_spec.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ box n (h.choose (p := fun (ν_1 : ι → ℤ) ↦ ν_1 ∈ admissibleIndex n B ∧ box n ν = box n ν_1)) = box n ν

Tactic:
exact h.choose_spec.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B I : Box ι
hI : I ∈ (prepartition n B).boxes
obtain :
  ∀ (ν : ι → ℤ) (hν : ν ∈ admissibleIndex n B) (hI : box n ν ∈ (prepartition n B).boxes),
    box n (index n ((prepartition n B).tag (box n ν))) = box n ν
⊢ box n (index n ((prepartition n B).tag I)) = I

Tactic:
obtain ⟨ν, hν, rfl⟩ := mem_prepartition_boxes_iff.mp hI

Premises used: BoxIntegral.unitPartition.mem_prepartition_boxes_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ (prepartition n B).boxes
rw : box n (index n (tag n ν)) = box n ν
rw₁ rw₂ : box n ν = box n ν
⊢ box n (index n ((prepartition n B).tag (box n ν))) = box n ν

Tactic:
rw [prepartition_tag n hν, index_tag]

Premises used: BoxIntegral.unitPartition.prepartition_tag, BoxIntegral.unitPartition.index_tag