awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 : ℝ)
⊢ x ≤ (↑a : ℝ) ↔ (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑a : ℝ)
have rw₇ : x ≤ (↑a : ℝ) ↔ x ≤ (↑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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ index n x ∈ admissibleIndex n B
have obtain : ∀ (l u : ι → ℤ) (hl : ∀ (i : ι), B.lower i = (↑(l i) : ℝ)) (hu : ∀ (i : ι), B.upper i = (↑(u i) : ℝ)),
  index n x ∈ admissibleIndex n B
Tactic: obtain ⟨l, u, hl, hu⟩ := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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) : ℝ)
⊢ index n x ∈ admissibleIndex n B
have 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) : ℝ)
Tactic: simp_rw [mem_admissibleIndex_iff, Box.le_iff_bounds, box_lower, box_upper, Pi.le_def,
    index_apply, hl, hu, ← forall_and]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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) : ℝ) ≤ HDiv.hDiv (α := ℝ) (↑(⌈(↑n : ℝ) * x x_1⌉ - 1) : ℝ) (↑n : ℝ) ∧
      HAdd.hAdd (α := ℝ) (↑(⌈(↑n : ℝ) * x x_1⌉ - 1) : ℝ) 1 / (↑n : ℝ) ≤ (↑(u x_1) : ℝ)
have 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) : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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) : ℝ)
have refine_1 : ∀ (i : ι), (↑(l i) : ℝ) ≤ HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 / (↑n : ℝ)
Tactic: refine fun i ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 : ℝ)
⊢ ∀ (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) : ℝ)
have refine_2 : ∀ (i : ι), (HSub.hSub (α := ℝ) (↑⌈(↑n : ℝ) * x i⌉ : ℝ) 1 + 1) / (↑n : ℝ) ≤ (↑(u i) : ℝ)
Tactic: refine fun i ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
⊢ (prepartition n B).IsPartition
have refine : ∀ (x : ι → ℝ) (hx : x ∈ B), box n (index n x) ∈ (prepartition n B).toPrepartition
Tactic: refine fun x hx ↦ ⟨box n (index n x), ?_, mem_box_iff_index.mpr rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
x : ι → ℝ
hx : x ∈ B
⊢ box n (index n x) ∈ (prepartition n B).toPrepartition
have rw : ∃ ν ∈ admissibleIndex n B, box n ν = box n (index n x)
Tactic: rw [TaggedPrepartition.mem_toPrepartition, mem_prepartition_iff]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
v : ι → ℝ
⊢ v ∈
      HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
have 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)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ v ∈
      HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
        (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ↔
    ∀ (i : ι), Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ)) ((↑n : ℝ) * v i)
have rw : (∀ (i : ι),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
      ((((Module.Basis.repr (Module.Basis.isUnitSMul (Pi.basisFun ℝ ι) (w := fun (x : ι) ↦ (↑n : ℝ)⁻¹) sorry) :
                  (a : ι → ℝ) → ι →₀ ℝ)
                v :
              ι →₀ ℝ) :
            (a : ι) → ℝ)
          i :
        ℝ)) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
v : ι → ℝ
this : Fintype ι
⊢ (∀ (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)
have simp_rw : (∀ (i : ι),
    Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
      (HSMul.hSMul (α := ℝˣ) (β := ℝ) (IsUnit.unit (a := (↑n : ℝ)⁻¹) sorry)⁻¹
        ((((Module.Basis.repr (Pi.basisFun ℝ ι) : (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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ (∀ (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)
have simp_rw₁ : (∀ (i : ι),
    Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
      (HSMul.hSMul (α := ℝˣ) (IsUnit.unit (a := (↑n : ℝ)⁻¹) sorry)⁻¹ (v 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ (∀ (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)
have simp_rw₂ : (∀ (i : ι),
    Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
      (HSMul.hSMul (α := ℝ) (↑(IsUnit.unit (a := (↑n : ℝ)⁻¹) sorry)⁻¹ : ℝ) (v 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ (∀ (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)
have simp_rw₃ : (∀ (i : ι),
    Membership.mem (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
      (HSMul.hSMul (α := ℝ) (↑(IsUnit.unit (a := (↑n : ℝ)⁻¹) sorry) : ℝ)⁻¹ (v 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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ (∀ (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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)
⊢ (∀ (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
ν : ι → ℤ
⊢ tag n ν ∈
    HSMul.hSMul (α := ℝ) (β := Submodule ℤ (ι → ℝ)) (↑n : ℝ)⁻¹
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
have refine : ∀ (i : ι), (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
Tactic: refine mem_smul_span_iff.mpr fun i ↦ ⟨ν i + 1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
ν : ι → ℤ
i : ι
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ))
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 (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
inst_1 : Finite ι
ν : ι → ℤ
i : ι
rw : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * (HAdd.hAdd (α := ℝ) (↑(ν i) : ℝ) 1 / (↑n : ℝ))
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₁ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * ((↑n : ℝ)⁻¹ * 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 (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)
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₂ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ)⁻¹ * 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 (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
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₃ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = 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 (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
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₄ : (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν 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 (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
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₅ : HAdd.hAdd (α := ℝ) (β := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i) : ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) 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 (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
⊢ (algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν i + 1) = (↑n : ℝ) * tag n ν i
have rw₆ : HAdd.hAdd (α := ℝ) (β := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) (ν 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]