awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B J : Box ι
hI : J ∈ prepartition n B
obtain :
  ∀ (ν : ι → ℤ) (hν : ν ∈ admissibleIndex n B) (hI : box n ν ∈ prepartition n B),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
      ((prepartition n B).tag (box n ν))
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) J : Set (ι → ℝ)) ((prepartition n B).tag J)

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

Premises used: BoxIntegral.unitPartition.mem_prepartition_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
rw : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
    ((prepartition n B).tag (box n ν))

Tactic:
rw [prepartition_tag n hν]

Premises used: BoxIntegral.unitPartition.prepartition_tag
-- 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
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)

Tactic:
Box.coe_subset_Icc (tag_mem _ _)

Premises used: BoxIntegral.unitPartition.tag_mem, BoxIntegral.Box.coe_subset_Icc
-- 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
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)

Tactic:
exact Box.coe_subset_Icc (tag_mem _ _)

Premises used: BoxIntegral.unitPartition.tag_mem, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
J : Box ι
hI : J ∈ prepartition n B
obtain :
  ∀ (ν : ι → ℤ) (hν : ν ∈ admissibleIndex n B) (hI : box n ν ∈ prepartition n B),
    (Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) ⊆
      Metric.closedBall ((prepartition n B).tag (box n ν))
        (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
              ((prepartition n B).tag (box n ν))) :
          ℝ)
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) J ⊆
    Metric.closedBall ((prepartition n B).tag J)
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag J)) :
        ℝ)

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

Premises used: BoxIntegral.unitPartition.mem_prepartition_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν))
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag (box n ν))) :
        ℝ)

Tactic:
fun _ h ↦ le_trans (Metric.dist_le_diam_of_mem (Box.isBounded_Icc _) h ?_) ?_

Premises used: Set.Mem, setOf, Set.Subset, Metric.dist_le_diam_of_mem, Metric.closedBall, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
refine_1 :
  ∀ (x : ι → ℝ)
    (h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
      ((prepartition n B).tag (box n ν))
refine_2 :
  ∀ (x : ι → ℝ)
    (h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x),
    Metric.diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν)) ≤
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag (box n ν))) :
        ℝ)
⊢ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) ⊆
    Metric.closedBall ((prepartition n B).tag (box n ν))
      (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
            ((prepartition n B).tag (box n ν))) :
        ℝ)

Tactic:
refine fun _ h ↦ le_trans (Metric.dist_le_diam_of_mem (Box.isBounded_Icc _) h ?_) ?_

Premises used: Metric.dist_le_diam_of_mem, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x
refine_1 : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ))
    ((prepartition n B).tag (box n ν))

Tactic:
rw [prepartition_tag n hν]

Premises used: BoxIntegral.unitPartition.prepartition_tag
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)

Tactic:
Box.coe_subset_Icc (tag_mem _ _)

Premises used: BoxIntegral.unitPartition.tag_mem, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x
⊢ Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) (tag n ν)

Tactic:
exact Box.coe_subset_Icc (tag_mem _ _)

Premises used: BoxIntegral.unitPartition.tag_mem, BoxIntegral.Box.coe_subset_Icc
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x
⊢ Metric.diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν)) ≤
    (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
          ((prepartition n B).tag (box n ν))) :
      ℝ)

Tactic:
le_trans (diam_boxIcc n ν) hn

Premises used: BoxIntegral.unitPartition.diam_boxIcc, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
r : ℝ
hr : 0 < r
hn : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ r
ν : ι → ℤ
hν : ν ∈ admissibleIndex n B
hI : box n ν ∈ prepartition n B
x : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν) : Set (ι → ℝ)) x
⊢ Metric.diam.{u_1} (α := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) (box n ν)) ≤
    (↑((fun (x : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) r hr)
          ((prepartition n B).tag (box n ν))) :
      ℝ)

Tactic:
exact le_trans (diam_boxIcc n ν) hn

Premises used: BoxIntegral.unitPartition.diam_boxIcc, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have h : 0 < (n : ℝ) := Nat.cast_pos.mpr <| n.pos_of_neZero
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑n : ℤ) * a + 1 = (↑n : ℤ) * a + 1
⊢ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 = (↑((↑n : ℤ) * a + 1) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1
rw₁ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) + 1 ≤ (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₂ : (↑a : ℝ) < x ↔ LE.le (α := ℝ) (↑((↑n : ℤ) * a + 1) : ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ)
rw₃ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a + 1 ≤ ⌈(↑n : ℝ) * x⌉
rw₄ : (↑a : ℝ) < x ↔ (↑n : ℤ) * a < ⌈(↑n : ℝ) * x⌉
rw₅ : (↑a : ℝ) < x ↔ (↑((↑n : ℤ) * a) : ℝ) < (↑n : ℝ) * x
rw₆ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
rw₇ : (↑a : ℝ) < x ↔ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) < (↑n : ℝ) * x
rw₈ rw₉ : (↑a : ℝ) < x ↔ (↑a : ℝ) < x
⊢ (↑a : ℝ) < x ↔ (↑a : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 / (↑n : ℝ)

Tactic:
rw [le_div_iff₀' h, le_sub_iff_add_le,
    show (n : ℝ) * a + 1 = (n * a + 1 : ℤ) by norm_cast,
    Int.cast_le, Int.add_one_le_iff, Int.lt_ceil, Int.cast_mul, Int.cast_natCast,
    mul_lt_mul_iff_right₀ h]

Premises used: Int.lt_ceil, Int.cast_natCast, le_div_iff₀', Int.cast_le, Int.add_one_le_iff, Int.cast_mul, mul_lt_mul_iff_right₀, le_sub_iff_add_le
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑n : ℤ) * a = (↑n : ℤ) * a
⊢ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ) = (↑((↑n : ℤ) * a) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
n : ℕ
inst : NeZero n
x : ℝ
a : ℤ
h : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x ≤ (↑a : ℝ) ↔ HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑n : ℝ) ≤ (↑a : ℝ)
rw₁ : x ≤ (↑a : ℝ) ↔ (↑⌈(↑n : ℝ) * x⌉ : ℝ) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
rw₂ : x ≤ (↑a : ℝ) ↔ LE.le (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) (↑((↑n : ℤ) * a) : ℝ)
rw₃ : x ≤ (↑a : ℝ) ↔ ⌈(↑n : ℝ) * x⌉ ≤ (↑n : ℤ) * a
rw₄ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ (↑((↑n : ℤ) * a) : ℝ)
rw₅ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ HMul.hMul (α := ℝ) (↑(↑n : ℤ) : ℝ) (↑a : ℝ)
rw₆ : x ≤ (↑a : ℝ) ↔ (↑n : ℝ) * x ≤ HMul.hMul (α := ℝ) (↑n : ℝ) (↑a : ℝ)
rw₇ rw₈ : x ≤ (↑a : ℝ) ↔ x ≤ (↑a : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)

Tactic:
rw [sub_add_cancel, div_le_iff₀' h,
    show (n : ℝ) * a = (n * a : ℤ) by norm_cast,
    Int.cast_le, Int.ceil_le, Int.cast_mul, Int.cast_natCast, mul_le_mul_iff_right₀ h]

Premises used: Int.cast_natCast, Int.cast_le, Int.cast_mul, Int.ceil_le, div_le_iff₀', sub_add_cancel, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
obtain :
  ∀ (l u : ι → ℤ) (hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)) (hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)),
    index n x ∈ admissibleIndex n B
⊢ index n x ∈ admissibleIndex n B

Tactic:
obtain ⟨l, u, hl, hu⟩ := hB
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
simp_rw :
  ∀ (x_1 : ι),
    (↑(l x_1) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑(⌈(↑n : ℝ) * x x_1⌉ - 1) : ℝ) (↑n : ℝ) ∧
      HAdd.hAdd (α := ℝ) (↑(⌈(↑n : ℝ) * x x_1⌉ - 1) : ℝ) 1 / (↑n : ℝ) ≤ (↑(u x_1) : ℝ)
⊢ index n x ∈ admissibleIndex n B

Tactic:
simp_rw [mem_admissibleIndex_iff, Box.le_iff_bounds, box_lower, box_upper, Pi.le_def,
    index_apply, hl, hu, ← forall_and]

Premises used: BoxIntegral.unitPartition.box_upper, BoxIntegral.unitPartition.mem_admissibleIndex_iff, BoxIntegral.Box.le_iff_bounds, BoxIntegral.unitPartition.box_lower, BoxIntegral.unitPartition.index_apply, Pi.le_def, forall_and
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
push_cast :
  ∀ (x_1 : ι),
    (↑(l x_1) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x x_1⌉ : ℝ) 1 / (↑n : ℝ) ∧
      (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x x_1⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u x_1) : ℝ)
⊢ ∀ (x_1 : ι),
    (↑(l x_1) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑(⌈(↑n : ℝ) * x x_1⌉ - 1) : ℝ) (↑n : ℝ) ∧
      HAdd.hAdd (α := ℝ) (↑(⌈(↑n : ℝ) * x x_1⌉ - 1) : ℝ) 1 / (↑n : ℝ) ≤ (↑(u x_1) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
⊢ ∀ (x_1 : ι),
    (↑(l x_1) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x x_1⌉ : ℝ) 1 / (↑n : ℝ) ∧
      (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x x_1⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u x_1) : ℝ)

Tactic:
fun i ↦ ⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
refine_1 : ∀ (i : ι), (↑(l i) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 / (↑n : ℝ)
refine_2 : ∀ (i : ι), (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u i) : ℝ)
⊢ ∀ (x_1 : ι),
    (↑(l x_1) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x x_1⌉ : ℝ) 1 / (↑n : ℝ) ∧
      (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x x_1⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u x_1) : ℝ)

Tactic:
refine fun i ↦ ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
i : ι
⊢ (↑(l i) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 / (↑n : ℝ)

Tactic:
(mem_admissibleIndex_of_mem_box_aux₁ n (x i) (l i)).mp ((hl i) ▸ (hx i).1)

Premises used: Eq.rec, And.left, Iff.mp, _private.0.BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box_aux₁
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
i : ι
⊢ (↑(l i) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 / (↑n : ℝ)

Tactic:
exact (mem_admissibleIndex_of_mem_box_aux₁ n (x i) (l i)).mp ((hl i) ▸ (hx i).1)

Premises used: Eq.rec, And.left, Iff.mp, _private.0.BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box_aux₁
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
i : ι
⊢ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u i) : ℝ)

Tactic:
(mem_admissibleIndex_of_mem_box_aux₂ n (x i) (u i)).mp ((hu i) ▸ (hx i).2)

Premises used: Eq.rec, And.right, Iff.mp, _private.0.BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box_aux₂
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
x : ι → ℝ
hx : x ∈ B
l u : ι → ℤ
hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)
hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)
i : ι
⊢ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u i) : ℝ)

Tactic:
exact (mem_admissibleIndex_of_mem_box_aux₂ n (x i) (u i)).mp ((hu i) ▸ (hx i).2)

Premises used: Eq.rec, And.right, Iff.mp, _private.0.BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box_aux₂
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
⊢ (prepartition n B).IsPartition

Tactic:
fun x hx ↦ ⟨box n (index n x), ?_, mem_box_iff_index.mpr rfl⟩

Premises used: Iff.mpr, BoxIntegral.unitPartition.index, BoxIntegral.Prepartition.IsPartition, And.intro, Exists.intro, BoxIntegral.unitPartition.mem_box_iff_index, BoxIntegral.TaggedPrepartition.IsPartition, BoxIntegral.unitPartition.box, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
refine : ∀ (x : ι → ℝ) (hx : x ∈ B), box n (index n x) ∈ (prepartition n B).toPrepartition
⊢ (prepartition n B).IsPartition

Tactic:
refine fun x hx ↦ ⟨box n (index n x), ?_, mem_box_iff_index.mpr rfl⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
rw : ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)
⊢ box n (index n x) ∈ (prepartition n B).toPrepartition

Tactic:
rw [TaggedPrepartition.mem_toPrepartition, mem_prepartition_iff]

Premises used: BoxIntegral.TaggedPrepartition.mem_toPrepartition, BoxIntegral.unitPartition.mem_prepartition_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)

Tactic:
⟨index n x, mem_admissibleIndex_of_mem_box n hB hx, rfl⟩

Premises used: BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box, BoxIntegral.unitPartition.index, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)

Tactic:
exact ⟨index n x, mem_admissibleIndex_of_mem_box n hB hx, rfl⟩
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
v : ι → ℝ
have :
  ∀ (this : Fintype ι),
    v ∈
        HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
          (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ↔
      ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
⊢ v ∈
      HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
v : ι → ℝ
this : Fintype ι
rw :
  (∀ (i : ι),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        ((((Module.Basis.repr (Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) ⋯) :
                    (a : ι → ℝ) → ι →₀ ℝ)
                  v :
                ι →₀ ℝ) :
              (a : ι) → ℝ)
            i :
          ℝ)) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
⊢ v ∈
      HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)

Tactic:
rw [ZSpan.smul _ (inv_ne_zero (NeZero.ne _)), Module.Basis.mem_span_iff_repr_mem]

Premises used: ZSpan.smul, Module.Basis.mem_span_iff_repr_mem
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
v : ι → ℝ
this : Fintype ι
simp_rw :
  (∀ (i : ι),
      Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        (HSMul.hSMul (α := ℝˣ) (β := ℝ) (IsUnit.unit (a := (↑n : ℝ)⁻¹) ⋯)⁻¹
          ((((Module.Basis.repr (Pi.basisFun ℝ ι) : (a : ι → ℝ) → ι →₀ ℝ) v : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
simp_rw₁ :
  (∀ (i : ι),
      Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        (HSMul.hSMul (α := ℝˣ) (IsUnit.unit (a := (↑n : ℝ)⁻¹) ⋯)⁻¹ (v i))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
simp_rw₂ :
  (∀ (i : ι),
      Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        (HSMul.hSMul (α := ℝ) (↑(IsUnit.unit (a := (↑n : ℝ)⁻¹) ⋯)⁻¹ : ℝ) (v i))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
simp_rw₃ :
  (∀ (i : ι),
      Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        (HSMul.hSMul (α := ℝ) (↑(IsUnit.unit (a := (↑n : ℝ)⁻¹) ⋯) : ℝ)⁻¹ (v i))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
simp_rw₄ :
  (∀ (i : ι),
      Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹⁻¹ (v i))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
simp_rw₅ :
  (∀ (i : ι),
      Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        (HSMul.hSMul (α := ℝ) (↑n : ℝ) (v i))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
⊢ (∀ (i : ι),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
        ((((Module.Basis.repr (Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) ⋯) :
                    (a : ι → ℝ) → ι →₀ ℝ)
                  v :
                ι →₀ ℝ) :
              (a : ι) → ℝ)
            i :
          ℝ)) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)

Tactic:
simp_rw [Module.Basis.repr_isUnitSMul, Pi.basisFun_repr, Units.smul_def, Units.val_inv_eq_inv_val,
    IsUnit.unit_spec, inv_inv, smul_eq_mul]

Premises used: Module.Basis.repr_isUnitSMul, Units.val_inv_eq_inv_val, Units.smul_def, inv_inv, smul_eq_mul, IsUnit.unit_spec, Pi.basisFun_repr
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
ν : ι → ℤ
⊢ tag n ν ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))

Tactic:
mem_smul_span_iff.mpr fun i ↦ ⟨ν i + 1, ?_⟩

Premises used: Iff.mpr, BoxIntegral.unitPartition.mem_smul_span_iff, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
ν : ι → ℤ
refine : ∀ (i : ι), (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
⊢ tag n ν ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))

Tactic:
refine mem_smul_span_iff.mpr fun i ↦ ⟨ν i + 1, ?_⟩

Premises used: Iff.mpr, BoxIntegral.unitPartition.mem_smul_span_iff, HAdd.hAdd, Exists.intro, OfNat.ofNat