awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
p : Box ι → Prop
⊢ (π.filter p).distortion ≤ π.distortion

Tactic:
sup_mono (filter_subset _ _)

Premises used: Finset.filter_subset, BoxIntegral.Prepartition.distortion, BoxIntegral.TaggedPrepartition.distortion, Finset.sup_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
p : Box ι → Prop
⊢ (π.filter p).distortion ≤ π.distortion

Tactic:
exact sup_mono (filter_subset _ _)

Premises used: Finset.filter_subset, Finset.sup_mono
-- Module: Mathlib.Analysis.BoxIntegral.Partition.Tagged
Goal:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst : Fintype ι
p : Box ι → Prop
⊢ (π.filter p).distortion ≤ π.distortion

Tactic:
classical exact sup_mono (filter_subset _ _)

Premises used: Finset.filter_subset, Finset.sup_mono
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
have : ∀ (this : Fintype ι), ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
obtain :
  ∀ (R : ℝ) (hR₁ : 0 < R) (hR₂ : s ⊆ Metric.ball 0 R), ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))

Tactic:
obtain ⟨R, hR₁, hR₂⟩ := IsBounded.subset_ball_lt h 0 0

Premises used: Bornology.IsBounded.subset_ball_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
⊢ 0 < ⌈R⌉₊

Tactic:
have hC := Nat.ceil_pos.mpr hR₁
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
x : ι
⊢ LT.lt (α := ℝ) ((fun (x : ι) ↦ (-(↑C : ℝ) : ℝ)) x) ((fun (x : ι) ↦ ((↑C : ℝ) : ℝ)) x)

Tactic:
simp [C, neg_lt_self_iff, Nat.cast_pos, hC]

Premises used: Nat.cast_pos, neg_lt_self_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))

Tactic:
⟨I, ⟨fun _ ↦ - C, fun _ ↦ C, fun i ↦ (Int.cast_neg_natCast C).symm, fun _ ↦ rfl⟩,
    le_trans hR₂ ?_⟩

Premises used: Int.cast_neg_natCast, Nat.cast, And.intro, Exists.intro, Eq.symm, Neg.neg, rfl, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
refine : Metric.ball 0 R ≤ (↑I : Set (ι → ℝ))
⊢ ∃ (B : Box ι), hasIntegralVertices B ∧ s ≤ (↑B : Set (ι → ℝ))

Tactic:
refine ⟨I, ⟨fun _ ↦ - C, fun _ ↦ C, fun i ↦ (Int.cast_neg_natCast C).symm, fun _ ↦ rfl⟩,
    le_trans hR₂ ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
suffices : Metric.ball 0 (↑C : ℝ) ≤ (↑I : Set (ι → ℝ))
⊢ Metric.ball 0 R ≤ (↑I : Set (ι → ℝ))

Tactic:
suffices Metric.ball (0 : ι → ℝ) C ≤ I from
    le_trans (Metric.ball_subset_ball (Nat.le_ceil R)) this
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) (Metric.ball 0 (↑C : ℝ)) x
⊢ ∀ (i : ι), -(↑⌈R⌉₊ : ℝ) < x i ∧ x i < (↑⌈R⌉₊ : ℝ)

Tactic:
simp_rw [C, mem_ball_zero_iff, pi_norm_lt_iff (Nat.cast_pos.mpr hC),
    Real.norm_eq_abs, abs_lt] at hx

Premises used: Iff.mpr, Nat.cast_pos, pi_norm_lt_iff, abs_lt, Real.norm_eq_abs, mem_ball_zero_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
x : ι → ℝ
hx : ∀ (i : ι), -(↑⌈R⌉₊ : ℝ) < x i ∧ x i < (↑⌈R⌉₊ : ℝ)
⊢ x ∈ (↑I : Set (ι → ℝ))

Tactic:
fun i ↦ ⟨(hx i).1, le_of_lt (hx i).2⟩

Premises used: Set.Ioc, Set.Mem, BoxIntegral.Box.toSet, setOf, le_of_lt, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℝ)
h : IsBounded s
this : Fintype ι
R : ℝ
hR₁ : 0 < R
hR₂ : s ⊆ Metric.ball 0 R
C : ℕ := ⌈R⌉₊
hC : 0 < ⌈R⌉₊
I : Box ι := { lower := fun (x : ι) ↦ -(↑C : ℝ), upper := fun (x : ι) ↦ (↑C : ℝ), lower_lt_upper := ⋯ }
x : ι → ℝ
hx : ∀ (i : ι), -(↑⌈R⌉₊ : ℝ) < x i ∧ x i < (↑⌈R⌉₊ : ℝ)
⊢ x ∈ (↑I : Set (ι → ℝ))

Tactic:
exact fun i ↦ ⟨(hx i).1, le_of_lt (hx i).2⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
⊢ HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑(ν x) : ℝ) 1 / (↑n : ℝ)

Tactic:
simp [add_div, n.pos_of_neZero]

Premises used: Nat.pos_of_neZero, add_div
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
⊢ (box n ν).lower = fun (i : ι) ↦ HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
⊢ (box n ν).upper = fun (i : ι) ↦ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
simp_rw :
  (∀ (i : ι), x i ∈ Set.Ioc ((box n ν).lower i) ((box n ν).upper i)) ↔
    ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
simp_rw₁ :
  (∀ (i : ι), x i ∈ Set.Ioc (HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ)) (HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ))) ↔
    ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
⊢ x ∈ box n ν ↔
    ∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)

Tactic:
simp_rw [Box.mem_def, box, Set.mem_Ioc]

Premises used: BoxIntegral.Box.mem_def, Set.mem_Ioc, BoxIntegral.unitPartition.box
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι → ℝ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
simp_rw :
  (∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)) ↔
    ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
simp_rw₁ :
  (∀ (i : ι), HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) < x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)) ↔
    ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)
⊢ x ∈ box n ν ↔ ∀ (i : ι), (↑(ν i) : ℝ) < (↑n : ℝ) * x i ∧ (↑n : ℝ) * x i ≤ HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1

Tactic:
simp_rw [mem_box_iff, ← _root_.le_div_iff₀' h, ← div_lt_iff₀' h]

Premises used: le_div_iff₀', BoxIntegral.unitPartition.mem_box_iff, div_lt_iff₀'
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
ν : ι → ℤ
i : ι
⊢ tag n ν i = HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
⊢ Function.Injective (β := ι → ℝ) fun (ν : ι → ℤ) ↦ tag n ν

Tactic:
fun _ _ h ↦ funext_iff.mpr fun i ↦ ?_

Premises used: Iff.mpr, funext_iff, Function.Injective
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
refine :
  ∀ (x x_1 : ι → ℤ) (h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1))
    (i : ι), x i = x_1 i
⊢ Function.Injective (β := ι → ℝ) fun (ν : ι → ℤ) ↦ tag n ν

Tactic:
refine fun _ _ h ↦ funext_iff.mpr fun i ↦ ?_

Premises used: Iff.mpr, funext_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x x_1 : ι → ℤ
h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1)
i : ι
⊢ Eq (α := ℝ) ((fun (x : ι → ℝ) ↦ x i) ((fun (ν : ι → ℤ) ↦ tag n ν) x))
    ((fun (x : ι → ℝ) ↦ x i) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1))

Tactic:
have := congr_arg (fun x ↦ x i) h
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x x_1 : ι → ℤ
h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1)
i : ι
this :
  Eq (α := ℝ) ((fun (x : ι → ℝ) ↦ x i) ((fun (ν : ι → ℤ) ↦ tag n ν) x))
    ((fun (x : ι → ℝ) ↦ x i) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1))
⊢ x i = x_1 i

Tactic:
simp_rw [tag_apply, div_left_inj' (c := (n : ℝ)) (Nat.cast_ne_zero.mpr (NeZero.ne n)),
    add_left_inj, Int.cast_inj] at this

Premises used: Iff.mpr, Int.cast_inj, add_left_inj, BoxIntegral.unitPartition.tag_apply, div_left_inj', Nat.cast_ne_zero, NeZero.ne
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x x_1 : ι → ℤ
h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1)
i : ι
this : x i = x_1 i
⊢ x i = x_1 i

Tactic:
this
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
x x_1 : ι → ℤ
h : Eq.{u_1 + 1} (α := ι → ℝ) ((fun (ν : ι → ℤ) ↦ tag n ν) x) ((fun (ν : ι → ℤ) ↦ tag n ν) x_1)
i : ι
this : x i = x_1 i
⊢ x i = x_1 i

Tactic:
exact this
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
⊢ tag n ν ∈ box n ν

Tactic:
mem_box_iff.mpr fun _ ↦ ?_

Premises used: Iff.mpr, BoxIntegral.unitPartition.mem_box_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
refine :
  ∀ (x : ι),
    HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < tag n ν x ∧ tag n ν x ≤ HAdd.hAdd (α := ℝ) (↑(ν x) : ℝ) 1 / (↑n : ℝ)
⊢ tag n ν ∈ box n ν

Tactic:
refine mem_box_iff.mpr fun _ ↦ ?_

Premises used: Iff.mpr, BoxIntegral.unitPartition.mem_box_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
rw :
  HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ∧
    HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
      HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < tag n ν x ∧ tag n ν x ≤ HAdd.hAdd (α := ℝ) (↑(ν x) : ℝ) 1 / (↑n : ℝ)

Tactic:
rw [tag, add_div]

Premises used: BoxIntegral.unitPartition.tag, add_div
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ 0 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
x : ι
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) < HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ∧
    HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤
      HDiv.hDiv (α := ℝ) (↑(ν x) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact ⟨lt_add_of_pos_right _ (by positivity), le_rfl⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
m : ℕ
x : ι → ℝ
i : ι
⊢ index m x i = ⌈(↑m : ℝ) * x i⌉ - 1

Tactic:
rfl

Premises used: BoxIntegral.unitPartition.index, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 : ℝ)
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 = ν

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]

Premises used: BoxIntegral.unitPartition.mem_box_iff', Int.ceil_eq_iff, funext_iff, Int.cast_add, BoxIntegral.unitPartition.index_apply, sub_eq_iff_eq_add, add_sub_cancel_right, Int.cast_one
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
⊢ index n (tag n ν) = ν

Tactic:
mem_box_iff_index.mp (tag_mem n ν)

Premises used: BoxIntegral.unitPartition.tag_mem, Iff.mp, BoxIntegral.unitPartition.mem_box_iff_index
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
rw : (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) ↔ ν = ν'
⊢ ν ≠ ν' ↔ Disjoint (↑(box n ν) : Set (ι → ℝ)) (↑(box n ν') : Set (ι → ℝ))

Tactic:
rw [not_iff_comm, Set.not_disjoint_iff]

Premises used: Set.not_disjoint_iff, not_iff_comm
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
⊢ (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) ↔ ν = ν'

Tactic:
⟨fun ⟨x, hx, hx'⟩ ↦ ?_, fun h ↦ ⟨tag n ν, tag_mem n ν, h ▸ tag_mem n ν⟩⟩

Premises used: BoxIntegral.unitPartition.tag_mem, _private.0.BoxIntegral.unitPartition.disjoint.match_1, BoxIntegral.unitPartition.tag, Eq.rec, And.intro, Iff.intro, Exists.intro, Eq
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν ν' : ι → ℤ
refine :
  (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) →
    ∀ (x : ι → ℝ) (hx : x ∈ (↑(box n ν) : Set (ι → ℝ))) (hx' : x ∈ (↑(box n ν') : Set (ι → ℝ))), ν = ν'
⊢ (∃ x ∈ (↑(box n ν) : Set (ι → ℝ)), x ∈ (↑(box n ν') : Set (ι → ℝ))) ↔ ν = ν'

Tactic:
refine ⟨fun ⟨x, hx, hx'⟩ ↦ ?_, fun h ↦ ⟨tag n ν, tag_mem n ν, h ▸ tag_mem n ν⟩⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 = ν'
rw₁ rw₂ : index n x = index n x
⊢ ν = ν'

Tactic:
rw [← mem_box_iff_index.mp hx, ← mem_box_iff_index.mp hx']

Premises used: Iff.mp, BoxIntegral.unitPartition.mem_box_iff_index
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
a₁ : ι → ℤ
_ :
  ∀ ⦃a₂ : ι → ℤ⦄, Eq.{u_1 + 1} (α := Box ι) ((fun (ν : ι → ℤ) ↦ box n ν) a₁) ((fun (ν : ι → ℤ) ↦ box n ν) a₂) → a₁ = a₂
⊢ ∀ ⦃a₂ : ι → ℤ⦄, Eq.{u_1 + 1} (α := Box ι) ((fun (ν : ι → ℤ) ↦ box n ν) a₁) ((fun (ν : ι → ℤ) ↦ box n ν) a₂) → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
a₁ a₂ : ι → ℤ
h : Eq.{u_1 + 1} (α := Box ι) ((fun (ν : ι → ℤ) ↦ box n ν) a₁) ((fun (ν : ι → ℤ) ↦ box n ν) a₂)
contrapose! : ∀ (h : a₁ ≠ a₂), box n a₁ ≠ box n a₂
⊢ a₁ = a₂

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
a₁ a₂ : ι → ℤ
h : a₁ ≠ a₂
⊢ box n a₁ ≠ box n a₂

Tactic:
Box.ne_of_disjoint_coe (disjoint.mp h)

Premises used: BoxIntegral.unitPartition.disjoint, BoxIntegral.Box.ne_of_disjoint_coe, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
a₁ a₂ : ι → ℤ
h : a₁ ≠ a₂
⊢ box n a₁ ≠ box n a₂

Tactic:
exact Box.ne_of_disjoint_coe (disjoint.mp h)

Premises used: BoxIntegral.unitPartition.disjoint, BoxIntegral.Box.ne_of_disjoint_coe, Iff.mp
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
ν : ι → ℤ
i : ι
simp_rw :
  HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ) - HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
simp_rw₁ :
  HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - HDiv.hDiv (α := ℝ) (↑(ν i) : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ (box n ν).upper i - (box n ν).lower i = HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
simp_rw [box, add_div, add_sub_cancel_left]

Premises used: add_sub_cancel_left, BoxIntegral.unitPartition.box, add_div
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
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 : ℝ)
⊢ Metric.diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν)) ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
rw [BoxIntegral.Box.Icc_eq_pi]

Premises used: BoxIntegral.Box.Icc_eq_pi
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
ν : ι → ℤ
refine :
  ∀ (i : ι),
    Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ 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:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) <| Metric.ediam_pi_le_of_le fun i ↦ ?_

Premises used: Metric.ediam_pi_le_of_le, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 : ℝ))
simp_rw₁ : ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ Metric.ediam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
simp_rw [Real.ediam_Icc, box.upper_sub_lower, le_rfl]

Premises used: le_rfl, BoxIntegral.unitPartition.box.upper_sub_lower, Real.ediam_Icc
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 ι))⁻¹
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 ι)

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]

Premises used: Iff.mpr, Finset.card_univ, MeasureTheory.volume_pi, Nat.cast_pos, ENNReal.ofReal_div_of_pos, Finset.prod_const, ENNReal.ofReal_one, Real.volume_Ioc, one_div, BoxIntegral.Box.coe_eq_pi, Nat.pos_of_neZero, BoxIntegral.unitPartition.box.upper_sub_lower, MeasureTheory.Measure.pi_pi, ENNReal.inv_pow, ENNReal.ofReal_natCast
-- 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)
⊢ 0 < 1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)

Tactic:
simp