awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
ν : ι → ℤ
i : ι
rw : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ))
rw₁ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * ((↑n : ℝ)⁻¹ * HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1)
rw₂ :
  (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ * HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
rw₃ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = 1 * HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
rw₄ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
rw₅ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i) : ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) 1 : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
rw₆ : HAdd.hAdd (α := ℝ) (β := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i) : ℝ) (1 : ℝ) = HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
rw₇ rw₈ : HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 = HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i

Tactic:
rw [tag_apply, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel_of_invertible, one_mul, map_add,
    map_one, eq_intCast]

Premises used: mul_inv_cancel_of_invertible, mul_assoc, map_add, eq_intCast, map_one, BoxIntegral.unitPartition.tag_apply, div_eq_inv_mul, one_mul
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx :
  x ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)

Tactic:
rw [mem_smul_span_iff] at hx

Premises used: BoxIntegral.unitPartition.mem_smul_span_iff
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)
h : ∀ (i : ι), tag n (index n x) i = x i
⊢ tag n (index n x) = x

Tactic:
ext i
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)
i : ι
⊢ ∃ (a : ℤ), (↑a : ℝ) = (↑n : ℝ) * x i

Tactic:
hx i

Premises used: Set.Mem, setOf, Set.range
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)
i : ι
h : ∀ (a : ℤ) (ha : (↑a : ℝ) = (↑n : ℝ) * x i), tag n (index n x) i = x i
⊢ tag n (index n x) i = x i

Tactic:
obtain ⟨a, ha⟩ : ∃ a : ℤ, a = n * x i := hx i
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)
i : ι
a : ℤ
ha : (↑a : ℝ) = (↑n : ℝ) * x i
h : HAdd.hAdd (α := ℝ) (↑(index n x i) : ℝ) 1 / (↑n : ℝ) = x i
h₁ : HAdd.hAdd (α := ℝ) (↑(⌈(↑n : ℝ) * x i⌉ - 1) : ℝ) 1 / (↑n : ℝ) = x i
h₂ : (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) (↑1 : ℝ) + 1) / (↑n : ℝ) = x i
h₃ : (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 + 1) / (↑n : ℝ) = x i
h₄ : HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) (↑n : ℝ) = x i
h₅ : HDiv.hDiv (α := ℝ) (↑(Int.ceil (α := ℝ) (↑a : ℝ)) : ℝ) (↑n : ℝ) = x i
h₆ : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑n : ℝ) = x i
h₇ : (↑a : ℝ) = x i * (↑n : ℝ)
h₈ h₉ h₁₀ h₁₁ : (↑a : ℝ) = (↑n : ℝ) * x i
⊢ tag n (index n x) i = x i

Tactic:
rwa [tag_apply, index_apply, Int.cast_sub, Int.cast_one, sub_add_cancel, ← ha, Int.ceil_intCast,
    div_eq_iff (NeZero.ne _), mul_comm]

Premises used: Int.cast_sub, Int.ceil_intCast, BoxIntegral.unitPartition.index_apply, div_eq_iff, mul_comm, BoxIntegral.unitPartition.tag_apply, sub_add_cancel, Int.cast_one, NeZero.ne
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x y : ι → ℝ
hx :
  x ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
hy :
  y ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
h : index n x = index n y
rw : tag n (index n x) = y
rw₁ : tag n (index n x) = tag n (index n y)
rw₂ rw₃ : tag n (index n y) = tag n (index n y)
⊢ x = y

Tactic:
rw [← tag_index_eq_self_of_mem_smul_span n hx, ← tag_index_eq_self_of_mem_smul_span n hy, h]

Premises used: BoxIntegral.unitPartition.tag_index_eq_self_of_mem_smul_span
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
c_1 : ℝ
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Finite ι
c : ℝ
hc : c ≠ 0
x : ι → ℝ
simp_rw :
  x ∈ s ∧ x ∈ c⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ↔
    Membership.mem (α := ι → ℝ) (c • s) ((Equiv.smulRight hc : (a : ι → ℝ) → ι → ℝ) x : ι → ℝ) ∧
      Membership.mem (α := ι → ℝ) (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
        ((Equiv.smulRight hc : (a : ι → ℝ) → ι → ℝ) x : ι → ℝ)
simp_rw₁ :
  x ∈ s ∧ x ∈ c⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ↔
    c • x ∈ c • s ∧ c • x ∈ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
simp_rw₂ :
  x ∈ s ∧ x ∈ c⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ↔
    x ∈ s ∧ c • x ∈ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ x ∈ s ∩ c⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ↔
    Membership.mem (α := ι → ℝ)
      (c • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
      ((Equiv.smulRight hc : (a : ι → ℝ) → ι → ℝ) x : ι → ℝ)

Tactic:
simp_rw [Set.mem_inter_iff, Equiv.smulRight_apply, Set.smul_mem_smul_set_iff₀ hc,
      ← Set.mem_inv_smul_set_iff₀ hc]

Premises used: Set.mem_inv_smul_set_iff₀, Set.mem_inter_iff, Set.smul_mem_smul_set_iff₀, Equiv.smulRight_apply
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
have :
  ∀ (this : Fintype ι),
    Nat.card.{u_1}
        (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1) ≤
      Nat.card.{u_1}
        (↑(s ∩ y⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)
⊢ Nat.card.{u_1}
      (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1) ≤
    Nat.card.{u_1}
      (↑(s ∩ y⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
rw :
  Nat.card.{u_1}
      (↑(x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1) ≤
    Nat.card.{u_1}
      (↑(y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)
⊢ Nat.card.{u_1}
      (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1) ≤
    Nat.card.{u_1}
      (↑(s ∩ y⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)

Tactic:
rw [Nat.card_congr (tendsto_card_div_pow₁ s hx.ne'),
      Nat.card_congr (tendsto_card_div_pow₁ s (hx.trans_le hy).ne')]

Premises used: _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₁, LT.lt.ne', Nat.card_congr, LT.lt.trans_le
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ Nat.card.{u_1}
      (↑(x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1) ≤
    Nat.card.{u_1}
      (↑(y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)

Tactic:
Nat.card_mono ?_ ?_

Premises used: Nat.card_mono
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
refine_1 : (y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite
refine_2 :
  x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ⊆
    y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ Nat.card.{u_1}
      (↑(x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1) ≤
    Nat.card.{u_1}
      (↑(y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)

Tactic:
refine Nat.card_mono ?_ ?_

Premises used: Nat.card_mono
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ (y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite

Tactic:
ZSpan.setFinite_inter _ (IsBounded.smul₀ hs₁ y)

Premises used: Set.Mem, setOf, Bornology.IsBounded.smul₀, ZSpan.setFinite_inter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ (y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite

Tactic:
exact ZSpan.setFinite_inter _ (IsBounded.smul₀ hs₁ y)

Premises used: Bornology.IsBounded.smul₀, ZSpan.setFinite_inter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ⊆
    y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
Set.inter_subset_inter_left _ <| hs₄ hx hy

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ⊆
    y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
exact Set.inter_subset_inter_left _ <| hs₄ hx hy

Premises used: Set.inter_subset_inter_left
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
h :
  (s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite
⊢ Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)

Tactic:
apply Set.Finite.fintype

Premises used: Set.Finite.fintype
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
h :
  (s ∩
      (↑(span ℤ
            (Set.range (ι := ι)
              (⇑(Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) ⋯) : (a : ι) → ι → ℝ))) :
        Set (ι → ℝ))).Finite
⊢ (s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite

Tactic:
rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]

Premises used: ZSpan.smul, Submodule.coe_pointwise_smul
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ (s ∩
      (↑(span ℤ
            (Set.range (ι := ι)
              (⇑(Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) ⋯) : (a : ι) → ι → ℝ))) :
        Set (ι → ℝ))).Finite

Tactic:
ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)

Premises used: BoxIntegral.Box.isBounded, Set.Mem, setOf, Bornology.IsBounded.subset, ZSpan.setFinite_inter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ (s ∩
      (↑(span ℤ
            (Set.range (ι := ι)
              (⇑(Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) ⋯) : (a : ι) → ι → ℝ))) :
        Set (ι → ℝ))).Finite

Tactic:
exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)

Premises used: BoxIntegral.Box.isBounded, Bornology.IsBounded.subset, ZSpan.setFinite_inter
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
have :
  ∀
    (this :
      Fintype
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
    ∑ J ∈ (prepartition n B).boxes,
        ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
              ℝ →L[ℝ] ℝ) :
            (a : ℝ) → ℝ)
          (s.indicator F ((prepartition n B).tag J)) =
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
⊢ ∑ J ∈ (prepartition n B).boxes,
      ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
            ℝ →L[ℝ] ℝ) :
          (a : ℝ) → ℝ)
        (s.indicator F ((prepartition n B).tag J)) =
    (∑' (x :
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
        F (↑x : ι → ℝ)) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)

Tactic:
have : Fintype ↑(s ∩ (n : ℝ)⁻¹ • L) := by
    apply Set.Finite.fintype
    rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]
    exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
rw :
  Eq (α := ℝ)
    (∑
      i ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset,
      F i / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    (∑ J ∈ (prepartition n B).boxes,
      ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
            ℝ →L[ℝ] ℝ) :
          (a : ℝ) → ℝ)
        (s.indicator F ((prepartition n B).tag J)))
⊢ ∑ J ∈ (prepartition n B).boxes,
      ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
            ℝ →L[ℝ] ℝ) :
          (a : ℝ) → ℝ)
        (s.indicator F ((prepartition n B).tag J)) =
    (∑' (x :
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
        F (↑x : ι → ℝ)) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)

Tactic:
rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]

Premises used: eq_comm, Finset.sum_div, tsum_fintype, Finset.sum_set_coe
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
simp_rw :
  Eq (α := ℝ)
    (∑
      i ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset,
      F i / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    (∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∈ s,
      Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑x : Set (ι → ℝ)) *
        F ((prepartition n B).tag x))
⊢ Eq (α := ℝ)
    (∑
      i ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset,
      F i / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    (∑ J ∈ (prepartition n B).boxes,
      ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
            ℝ →L[ℝ] ℝ) :
          (a : ℝ) → ℝ)
        (s.indicator F ((prepartition n B).tag J)))

Tactic:
simp_rw [Set.indicator_apply, apply_ite, BoxAdditiveMap.toSMul_apply, Measure.toBoxAdditive_apply,
    smul_eq_mul, mul_zero, Finset.sum_ite, Finset.sum_const_zero, add_zero]

Premises used: Set.indicator_apply, apply_ite, Finset.sum_const_zero, MulZeroClass.mul_zero, BoxIntegral.BoxAdditiveMap.toSMul_apply, MeasureTheory.Measure.toBoxAdditive_apply, smul_eq_mul, add_zero, Finset.sum_ite
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
⊢ Eq (α := ℝ)
    (∑
      i ∈
        (s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset,
      F i / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    (∑ x ∈ (prepartition n B).boxes with (prepartition n B).tag x ∈ s,
      Measure.real (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ)) (↑x : Set (ι → ℝ)) *
        F ((prepartition n B).tag x))

Tactic:
Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_)
    (fun _ hx _ hy h ↦ ?_) (fun I hI ↦ ?_) (fun _ hx ↦ ?_)

Premises used: Iff.mpr, Finset.sum_bij, BoxIntegral.unitPartition.index, Finset.mem_filter, BoxIntegral.unitPartition.box
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
⊢ x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
rw [Set.mem_toFinset] at hx

Premises used: Set.mem_toFinset
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx_1 :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hx :
  x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ (fun (x : ι → ℝ)
            (x_1 :
              x ∈
                (s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset) ↦
          box n (index n x))
        x hx_1 ∈
      (prepartition n B).boxes ∧
    (prepartition n B).tag
        ((fun (x : ι → ℝ)
              (x_1 :
                x ∈
                  (s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                          Set (ι → ℝ))).toFinset) ↦
            box n (index n x))
          x hx_1) ∈
      s

Tactic:
⟨mem_prepartition_boxes_iff.mpr
      ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩

Premises used: Iff.mpr, BoxIntegral.unitPartition.mem_prepartition_boxes_iff, BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box, BoxIntegral.unitPartition.index, And.left, And.intro, Exists.intro, rfl