awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊x⌋₊
h :
  (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) *
      (HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) / x ^ card ι) =
    (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι
h₁ :
  (↑(Nat.card.{u_1}
                (↑(s ∩
                      HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_1)) :
            ℝ) /
          HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) *
        HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι) /
      x ^ card ι =
    (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι
h₂ h₃ :
  (↑(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 ∩
                  HSMul.hSMul (α := ℝ) (↑⌊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)) :
          ℝ) /
        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 ι

Tactic:
rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]

Premises used: mul_div, div_mul_cancel₀, 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
⊢ HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.BoxIntegral.UnitPartition
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
x : ℝ
hx : 1 ≤ x
h :
  (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι) *
      (HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι) / x ^ card ι) =
    (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι
h₁ :
  (↑(Nat.card.{u_1}
                (↑(s ∩
                      HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_1)) :
            ℝ) /
          HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι) *
        HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι) /
      x ^ card ι =
    (↑(Nat.card.{u_1}
            (↑(s ∩
                  HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_1)) :
        ℝ) /
      x ^ card ι
h₂ h₃ :
  (↑(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 ∩
                  HSMul.hSMul (α := ℝ) (↑⌈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)) :
          ℝ) /
        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 ι

Tactic:
rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]

Premises used: mul_div, div_mul_cancel₀, div_pow
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume s =
    Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)

Tactic:
ring
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
rw :
  Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))
⊢ Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))

Tactic:
rw [show volume.real s = volume.real s * 1 ^ card ι by ring]
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        x ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le' ?_ ?_
    (tendsto_card_div_pow₃ s hs₁ hs₄) (tendsto_card_div_pow₄ s hs₁ hs₄)

Premises used: _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₄, tendsto_of_tendsto_of_tendsto_of_le_of_le', _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₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (b : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊b⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        b ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))

Tactic:
Tendsto.congr' (tendsto_card_div_pow₅ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))

Premises used: _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₅, Filter.Tendsto.pow, Filter.Tendsto.mul, Filter.Tendsto.congr'
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
refine_1 :
  Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))
refine_1₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ) / x) atTop (𝓝 1)
⊢ Tendsto
    (fun (b : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊b⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        b ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))

Tactic:
refine Tendsto.congr' (tendsto_card_div_pow₅ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))

Premises used: _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₅, Filter.Tendsto.pow, Filter.Tendsto.mul, Filter.Tendsto.congr'
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))

Tactic:
Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_floor_atTop

Premises used: tendsto_card_div_pow_atTop_volume, tendsto_nat_floor_atTop, Filter.Tendsto.comp
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌊x⌋₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌊x⌋₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))

Tactic:
exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_floor_atTop

Premises used: tendsto_card_div_pow_atTop_volume, tendsto_nat_floor_atTop, Filter.Tendsto.comp
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ) / x) atTop (𝓝 1)

Tactic:
tendsto_nat_floor_div_atTop

Premises used: tendsto_nat_floor_div_atTop
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ) / x) atTop (𝓝 1)

Tactic:
exact tendsto_nat_floor_div_atTop

Premises used: tendsto_nat_floor_div_atTop
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (b : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈b⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        b ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))

Tactic:
Tendsto.congr' (tendsto_card_div_pow₆ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))

Premises used: Filter.Tendsto.pow, _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₆, Filter.Tendsto.mul, Filter.Tendsto.congr'
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
refine_2 :
  Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))
refine_2₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌈x⌉₊ : ℝ) / x) atTop (𝓝 1)
⊢ Tendsto
    (fun (b : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈b⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        b ^ card ι)
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s * HPow.hPow (α := ℝ) 1 (card ι)))

Tactic:
refine Tendsto.congr' (tendsto_card_div_pow₆ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))

Premises used: Filter.Tendsto.pow, _private.0.BoxIntegral.unitPartition.tendsto_card_div_pow₆, Filter.Tendsto.mul, Filter.Tendsto.congr'
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))

Tactic:
Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_ceil_atTop

Premises used: tendsto_card_div_pow_atTop_volume, tendsto_nat_ceil_atTop, Filter.Tendsto.comp
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto
    (fun (x : ℝ) ↦
      (↑(Nat.card.{u_1}
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑⌈x⌉₊ : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) (card ι))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s))

Tactic:
exact Tendsto.comp (tendsto_card_div_pow_atTop_volume s hs₁ hs₂ hs₃) tendsto_nat_ceil_atTop

Premises used: tendsto_card_div_pow_atTop_volume, tendsto_nat_ceil_atTop, Filter.Tendsto.comp
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌈x⌉₊ : ℝ) / x) atTop (𝓝 1)

Tactic:
tendsto_nat_ceil_div_atTop

Premises used: tendsto_nat_ceil_div_atTop
-- 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)
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌈x⌉₊ : ℝ) / x) atTop (𝓝 1)

Tactic:
exact tendsto_nat_ceil_div_atTop

Premises used: tendsto_nat_ceil_div_atTop
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := Set A) (Set.Ici 0) a
b : A
hb : Membership.mem (γ := Set A) (Set.Ici 0) b
hab : a ≤ b
⊢ 0 ≤ a

Tactic:
simp only [Set.mem_Ici] at ha hb

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a : A
ha : Membership.mem (γ := Set A) (Set.Ici 0) a
b : A
hb : Membership.mem (γ := Set A) (Set.Ici 0) b
hab : a ≤ b
ha₁ : 0 ≤ a
⊢ 0 ≤ b

Tactic:
simp only [Set.mem_Ici] at ha hb

Premises used: Set.mem_Ici
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
rw :
  cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (↑a : Unitization ℂ A) ≤
    cfc (p := fun (x : Unitization ℂ A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) (↑b : Unitization ℂ A)
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) a ≤
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ 1 - (1 + x)⁻¹) b

Tactic:
rw [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _]

Premises used: Unitization.inr_le_iff, Unitization.nnreal_cfcₙ_eq_cfc_inr
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)

Tactic:
rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab

Premises used: Unitization.inr_le_iff, IsSelfAdjoint.of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hab₁ : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
⊢ 0 ≤ a

Tactic:
rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab

Premises used: Unitization.inr_le_iff, IsSelfAdjoint.of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hab₁ : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha₁ : 0 ≤ a
⊢ 0 ≤ b

Tactic:
rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab

Premises used: Unitization.inr_le_iff, IsSelfAdjoint.of_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : 0 ≤ a
hb : 0 ≤ b
⊢ LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)

Tactic:
rw [← inr_nonneg_iff] at ha hb

Premises used: Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : 0 ≤ a
hb : 0 ≤ b
ha₁ : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
⊢ LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)

Tactic:
rw [← inr_nonneg_iff] at ha hb

Premises used: Unitization.inr_nonneg_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Goal:
A : Type u_1
inst : NonUnitalCStarAlgebra A
inst_1 : PartialOrder A
inst_2 : StarOrderedRing A
a b : A
hab : LE.le (α := Unitization ℂ A) (↑a : Unitization ℂ A) (↑b : Unitization ℂ A)
ha : LE.le (α := Unitization ℂ A) 0 (↑a : Unitization ℂ A)
hb : LE.le (α := Unitization ℂ A) 0 (↑b : Unitization ℂ A)
c : Unitization ℂ A
hc : 0 ≤ c
x : ℝ≥0
h : x ∈ σ ℝ≥0 c
⊢ (1 + x)⁻¹ ≤ 1

Tactic:
simp