awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : (prepartition n B).IsSubordinate (r 0)
⊢ dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2
have refine_2 : IntegrationParams.Riemann.bHenstock = true → (prepartition n B).IsHenstock
Tactic: refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : (prepartition n B).IsSubordinate (r 0)
refine_2 : IntegrationParams.Riemann.bHenstock = true → (prepartition n B).IsHenstock
⊢ dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2
have refine_3 : ∀ (h : IntegrationParams.Riemann.bDistortion = true), (prepartition n B).distortion ≤ 0
Tactic: refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
refine_1 : (prepartition n B).IsSubordinate (r 0)
refine_2 : IntegrationParams.Riemann.bHenstock = true → (prepartition n B).IsHenstock
refine_3 : ∀ (h : IntegrationParams.Riemann.bDistortion = true), (prepartition n B).distortion ≤ 0
⊢ dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2
have refine_4 : ∀ (h : IntegrationParams.Riemann.bDistortion = true),
  ∃ (π' : Prepartition B), π'.iUnion = (↑B : Set (ι → ℝ)) \ (prepartition n B).iUnion ∧ π'.distortion ≤ 0
Tactic: refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
⊢ (prepartition n B).IsSubordinate (r 0)
have refine_1 : (prepartition n B).IsSubordinate fun (x : ι → ℝ) ↦ r 0 0
Tactic: rw [show r 0 = fun _ ↦ r 0 0 from funext_iff.mpr (hr₁ 0 rfl)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
⊢ (prepartition n B).IsSubordinate fun (x : ι → ℝ) ↦ r 0 0
have refine_1 : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑(r 0 0) : ℝ)
Tactic: apply prepartition_isSubordinate n B
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ (↑(r 0 0) : ℝ)
have refine_1 : (↑(r 0 0) : ℝ)⁻¹ ≤ (↑n : ℝ)
Tactic: rw [one_div, inv_le_comm₀ (mod_cast (Nat.pos_of_neZero n)) (r 0 0).prop]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))
have h : ∀ (x : ℕ),
  Eq (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    (∑' (x :
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1)),
      1)
Tactic: convert! tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
h :
  ∀ (x : ℕ),
    Eq (α := ℝ)
      (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ)
      (∑' (x :
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
        1)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))
have h₁ : Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
  @MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦ 1
Tactic: convert! tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
x : ℕ
⊢ Eq (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    (∑' (x :
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1)),
      1)
have h : (↑(Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)) :
    ℝ) =
  HSMul.hSMul (β := ℝ)
    (Nat.card.{u_1}
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1))
    1
Tactic: rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
x : ℕ
h :
  (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ) =
    HSMul.hSMul (β := ℝ)
      (Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1))
      1
⊢ Eq (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    (∑' (x :
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1)),
      1)
have h₁ : (↑(Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)) :
    ℝ) =
  HMul.hMul (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    1
Tactic: rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
x : ℕ
h :
  (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ) =
    HSMul.hSMul (β := ℝ)
      (Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1))
      1
h₁ :
  (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ) =
    HMul.hMul (α := ℝ)
      (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ)
      1
⊢ Eq (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    (∑' (x :
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1)),
      1)
have h₂ : Eq (α := ℝ)
  (↑(Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)) :
    ℝ)
  (↑(Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)) :
    ℝ)
Tactic: rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
x : ℕ
h :
  (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ) =
    HSMul.hSMul (β := ℝ)
      (Nat.card.{u_1}
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1))
      1
h₁ :
  (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ) =
    HMul.hMul (α := ℝ)
      (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ)
      1
h₂ :
  Eq (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
⊢ Eq (α := ℝ)
    (↑(Nat.card.{u_1}
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)) :
      ℝ)
    (∑' (x :
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1)),
      1)
have h₃ : Nat.card.{u_1}
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1) =
  Nat.card.{u_1}
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑x : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
Tactic: rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    @MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦ 1
have h : Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
  HSMul.hSMul (β := ℝ) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s) 1
Tactic: rw [setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
h :
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    HSMul.hSMul (β := ℝ) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s) 1
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    @MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦ 1
have h₁ : Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * 1
Tactic: rw [setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
h :
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    HSMul.hSMul (β := ℝ) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s) 1
h₁ :
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * 1
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    @MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦ 1
have h₂ : Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s
Tactic: rw [setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ ∀ᶠ (x : ℝ) in atTop,
    (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι ≤
      (↑(Nat.card.{u_1}
              (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι
have h : ∀ (x : ℝ) (hx : 1 ≤ x),
  (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι ≤
    (↑(Nat.card.{u_1}
            (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι
Tactic: filter_upwards [eventually_ge_atTop 1] with x hx