awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
⊢ (↑(r 0 0) : ℝ)⁻¹ ≤ (↑n : ℝ)

Tactic:
le_trans (Nat.le_ceil _) (Nat.cast_le.mpr hn)

Premises used: Iff.mpr, Nat.le_ceil, Nat.cast_le, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
⊢ (↑(r 0 0) : ℝ)⁻¹ ≤ (↑n : ℝ)

Tactic:
exact le_trans (Nat.le_ceil _) (Nat.cast_le.mpr hn)

Premises used: Iff.mpr, Nat.le_ceil, Nat.cast_le, le_trans
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
h : IntegrationParams.Riemann.bHenstock = true
⊢ (prepartition n B).IsHenstock

Tactic:
prepartition_isHenstock n B

Premises used: BoxIntegral.unitPartition.prepartition_isHenstock
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
h : IntegrationParams.Riemann.bHenstock = true
⊢ (prepartition n B).IsHenstock

Tactic:
exact prepartition_isHenstock n B

Premises used: BoxIntegral.unitPartition.prepartition_isHenstock
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
h : IntegrationParams.Riemann.bDistortion = true
⊢ (prepartition n B).distortion ≤ 0

Tactic:
simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h

Premises used: Bool.false_eq_true, BoxIntegral.IntegrationParams.Riemann
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
h : IntegrationParams.Riemann.bDistortion = true
⊢ ∃ (π' : Prepartition B), π'.iUnion = (↑B : Set (ι → ℝ)) \ (prepartition n B).iUnion ∧ π'.distortion ≤ 0

Tactic:
simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h

Premises used: Bool.false_eq_true, BoxIntegral.IntegrationParams.Riemann
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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 : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          (fun (x : ι → ℝ) ↦ (1 : ℝ)) (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        (fun (x : ι → ℝ) ↦ (1 : ℝ)) x))

Tactic:
tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃

Premises used: tendsto_tsum_div_pow_atTop_integral, continuous_const, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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)
h₁ :
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    @MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦ 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))

Tactic:
convert! tendsto_tsum_div_pow_atTop_integral s (fun _ ↦ 1) continuous_const hs₁ hs₂ hs₃

Premises used: tendsto_tsum_div_pow_atTop_integral, continuous_const, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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)) :
      ℝ)
h₃ 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)
⊢ 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:
rw [tsum_const, nsmul_eq_mul, mul_one, Nat.cast_inj]

Premises used: Nat.cast_inj, nsmul_eq_mul, mul_one, tsum_const
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
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
h₂ h₃ :
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    Measure.real (m := MeasureSpace.toMeasurableSpace) volume s
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    @MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦ 1

Tactic:
rw [setIntegral_const, smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one, MeasureTheory.setIntegral_const
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
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 ι
⊢ ∀ᶠ (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 ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
h :
  Nat.card.{u_1}
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
              (↑(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 ∩
                  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:
gcongr
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ Nat.card.{u_1}
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
              (↑(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)

Tactic:
tendsto_card_div_pow₂ s hs₁ hs₄ (Nat.cast_pos.mpr (Nat.floor_pos.mpr hx))
    (Nat.floor_le (zero_le_one.trans hx))

Premises used: Iff.mpr, Nat.cast_pos, zero_le_one, Nat.floor_le, _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₂, LE.le.trans, Nat.floor_pos
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 1 ≤ x
⊢ Nat.card.{u_1}
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
              (↑(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)

Tactic:
exact tendsto_card_div_pow₂ s hs₁ hs₄ (Nat.cast_pos.mpr (Nat.floor_pos.mpr hx))
    (Nat.floor_le (zero_le_one.trans hx))

Premises used: Iff.mpr, Nat.cast_pos, zero_le_one, Nat.floor_le, _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₂, LE.le.trans, Nat.floor_pos
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
h :
  ∀ (x : ℝ) (hx : 0 < x),
    (↑(Nat.card.{u_1}
              (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι ≤
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι
⊢ ∀ᶠ (x : ℝ) in atTop,
    (↑(Nat.card.{u_1}
              (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι ≤
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
h :
  Nat.card.{u_1}
      (↑(s ∩ 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)
⊢ (↑(Nat.card.{u_1}
            (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι ≤
    (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι

Tactic:
gcongr
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
⊢ Nat.card.{u_1}
      (↑(s ∩ 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:
tendsto_card_div_pow₂ s hs₁ hs₄ hx (Nat.le_ceil _)

Premises used: Nat.le_ceil, _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₂
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
hs₁ : Bornology.IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x : ℝ
hx : 0 < x
⊢ Nat.card.{u_1}
      (↑(s ∩ 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:
exact tendsto_card_div_pow₂ s hs₁ hs₄ hx (Nat.le_ceil _)

Premises used: Nat.le_ceil, _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₂
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
h :
  ∀ (x : ℝ) (hx : 1 ≤ x),
    (↑(Nat.card.{u_1}
                (↑(s ∩
                      HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_1)) :
            ℝ) /
          HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) *
        ((↑⌊x⌋₊ : ℝ) / x) ^ card ι =
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι
⊢ EventuallyEq (β := ℝ) atTop
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
                (↑(s ∩
                      HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_1)) :
            ℝ) /
          HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) *
        ((↑⌊x⌋₊ : ℝ) / x) ^ card ι)
    fun (x : ℝ) ↦
    (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
x : ℝ
hx : 1 ≤ x
⊢ 0 < ⌊x⌋₊

Tactic:
have : 0 < ⌊x⌋₊ := Nat.floor_pos.mpr hx
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
⊢ HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) ≠ 0

Tactic:
positivity