-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem _root_.tendsto_card_div_pow_atTop_volume' (hs₁ : IsBounded s)
    (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0)
    (hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s) :
    Tendsto (fun x : ℝ ↦ (Nat.card ↑(s ∩ x⁻¹ • L) : ℝ) / x ^ card ι)
      atTop (nhds (volume s).toReal)

Proof state:
case refine_2.refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑⌈x⌉₊ / x) atTop (nhds 1)

Tactic:
exact tendsto_nat_ceil_div_atTop

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι) atTop
    (nhds ((volume s).toReal * 1 ^ card ι))

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

Result:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun b => ↑(Nat.card ↑(s ∩ (↑⌊b⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / b ^ card ι) atTop
    (nhds ((volume s).toReal * 1 ^ card ι))

case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun b => ↑(Nat.card ↑(s ∩ (↑⌈b⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / b ^ card ι) atTop
    (nhds ((volume s).toReal * 1 ^ card ι))

Proof state:
case refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun b => ↑(Nat.card ↑(s ∩ (↑⌊b⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / b ^ card ι) atTop
    (nhds ((volume s).toReal * 1 ^ card ι))

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

Result:
case refine_1.refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι) atTop
    (nhds (volume s).toReal)

case refine_1.refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑⌊x⌋₊ / x) atTop (nhds 1)

Proof state:
case refine_1.refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ (↑⌊x⌋₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌊x⌋₊ ^ card ι) atTop
    (nhds (volume s).toReal)

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

Result:
no goals

Proof state:
case refine_1.refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑⌊x⌋₊ / x) atTop (nhds 1)

Tactic:
exact tendsto_nat_floor_div_atTop

Result:
no goals

Proof state:
case refine_2.refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι) atTop
    (nhds (volume s).toReal)

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

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun b => ↑(Nat.card ↑(s ∩ (↑⌈b⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / b ^ card ι) atTop
    (nhds ((volume s).toReal * 1 ^ card ι))

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

Result:
case refine_2.refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ (↑⌈x⌉₊)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / ↑⌈x⌉₊ ^ card ι) atTop
    (nhds (volume s).toReal)

case refine_2.refine_2
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑⌈x⌉₊ / x) atTop (nhds 1)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι) atTop
    (nhds (volume s).toReal)

Tactic:
rw [show (volume s).toReal = (volume s).toReal * 1 ^ card ι by ring]

Result:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ Tendsto (fun x => ↑(Nat.card ↑(s ∩ x⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))) / x ^ card ι) atTop
    (nhds ((volume s).toReal * 1 ^ card ι))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
⊢ (volume s).toReal = (volume s).toReal * 1 ^ card ι

Tactic:
ring

Result:
no goals