awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ
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 ι
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 ∩ x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) : Type u_1)
Tactic: gcongr
-- 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 ∩ 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 ι
have 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 ι
Tactic: filter_upwards [eventually_gt_atTop 0] with x hx
-- 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 : ℝ
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 ι
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
⊢ 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 ι
have 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 ι
Tactic: filter_upwards [eventually_ge_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
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 ι
have this : 0 < ⌊x⌋₊
Tactic: have : 0 < ⌊x⌋₊ := Nat.floor_pos.mpr hx
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
x : ℝ
hx : 1 ≤ x
this : 0 < ⌊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 ι
have 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 ι
Tactic: rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 ι
⊢ (↑(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 ι
have 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 ι
Tactic: rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 ι
⊢ (↑(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 ι
have 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 ι
Tactic: rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
⊢ 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 ι
have 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 ι
Tactic: filter_upwards [eventually_ge_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
inst : Fintype ι
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 ι
have 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 ι
Tactic: rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 ι
⊢ (↑(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 ι
have 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 ι
Tactic: rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
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 ι
⊢ (↑(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 ι
have 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 ι
Tactic: rw [div_pow, mul_div, div_mul_cancel₀ _ (by positivity)]
-- 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)
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))
have 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 ι)))
Tactic: rw [show volume.real s = volume.real s * 1 ^ card ι by ring]
-- 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)
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 ι)))
have 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))
Tactic: refine Tendsto.congr' (tendsto_card_div_pow₅ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))
-- 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)
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))
⊢ 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 ι)))
have refine_1₁ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (↑⌊x⌋₊ : ℝ) / x) atTop (𝓝 1)
Tactic: refine Tendsto.congr' (tendsto_card_div_pow₅ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))
-- 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)
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 ι)))
have 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))
Tactic: refine Tendsto.congr' (tendsto_card_div_pow₆ s) (Tendsto.mul ?_ (Tendsto.pow ?_ _))