awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : 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
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₇ : HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 = HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1
Tactic: rw [tag_apply, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel_of_invertible, one_mul, map_add,
    map_one, eq_intCast]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx :
  x ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ tag n (index n x) = x
have hx₁ : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)
Tactic: rw [mem_smul_span_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
x : ι → ℝ
hx : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * x i)
⊢ tag n (index n x) = x
have h : ∀ (i : ι), tag n (index n x) i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 : ι
⊢ tag n (index n x) i = x i
have h : ∀ (a : ℤ) (ha : (↑a : ℝ) = (↑n : ℝ) * x i), tag n (index n x) i = x i
Tactic: obtain ⟨a, ha⟩ : ∃ a : ℤ, a = n * x i := hx i
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h : HAdd.hAdd (α := ℝ) (↑(index n x i) : ℝ) 1 / (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₁ : HAdd.hAdd (α := ℝ) (↑(⌈(↑n : ℝ) * x i⌉ - 1) : ℝ) 1 / (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₂ : (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) (↑1 : ℝ) + 1) / (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₃ : (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 + 1) / (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₄ : HDiv.hDiv (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₅ : HDiv.hDiv (α := ℝ) (↑(Int.ceil (α := ℝ) (↑a : ℝ)) : ℝ) (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₆ : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑n : ℝ) = 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ tag n (index n x) i = x i
have h₇ : (↑a : ℝ) = x i * (↑n : ℝ)
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ x = y
have rw : tag n (index n 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ x = y
have rw₁ : tag n (index n x) = tag n (index n y)
Tactic: rw [← tag_index_eq_self_of_mem_smul_span n hx, ← tag_index_eq_self_of_mem_smul_span n hy, h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ x = y
have rw₂ : tag n (index n y) = tag n (index n y)
Tactic: rw [← tag_index_eq_self_of_mem_smul_span n hx, ← tag_index_eq_self_of_mem_smul_span n hy, h]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
c_1 : ℝ
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Finite ι
c : ℝ
hc : c ≠ 0
x : ι → ℝ
⊢ 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 : ι → ℝ)
have 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 : ι → ℝ)
Tactic: simp_rw [Set.mem_inter_iff, Equiv.smulRight_apply, Set.smul_mem_smul_set_iff₀ hc,
      ← Set.mem_inv_smul_set_iff₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 : ι → ℝ)
⊢ 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 : ι → ℝ)
have 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 (ι → ℝ))
Tactic: simp_rw [Set.mem_inter_iff, Equiv.smulRight_apply, Set.smul_mem_smul_set_iff₀ hc,
      ← Set.mem_inv_smul_set_iff₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 (ι → ℝ))
⊢ 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 : ι → ℝ)
have simp_rw₂ : x ∈ s ∧ x ∈ c⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ↔
  x ∈ s ∧ c • x ∈ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
Tactic: simp_rw [Set.mem_inter_iff, Equiv.smulRight_apply, Set.smul_mem_smul_set_iff₀ hc,
      ← Set.mem_inv_smul_set_iff₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ 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)
have 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)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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}
      (↑(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)
have 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)
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')]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
have refine_1 : (y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite
Tactic: refine Nat.card_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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
⊢ 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)
have refine_2 : x • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) ⊆
  y • s ∩ (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
Tactic: refine Nat.card_mono ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
have h : (s ∩
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite
Tactic: apply Set.Finite.fintype
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ (s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).Finite
have h : (s ∩
    (↑(span ℤ
          (Set.range (ι := ι)
            (⇑(Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) sorry) : (a : ι) → ι → ℝ))) :
      Set (ι → ℝ))).Finite
Tactic: rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ ∑ 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 ι)
have 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 ι)
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₀)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ ∑ 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 ι)
have 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)))
Tactic: rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 ι))
    (∑ 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)))
have 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))
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]