-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
L : Submodule ℤ E
inst_2 : DiscreteTopology.{u_1} ↥L
inst_3 : IsZLattice ℝ L
ι : Type u_2
inst_4 : Fintype ι
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
inst_5 : FiniteDimensional ℝ E
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier
          (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
            {x : E | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)
refine_1 :
  EventuallyEq (β := ℝ) atTop
    ((fun (x : ℝ) ↦
        (↑(Nat.card.{u_2}
                (↑(Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
                        {x : E | x ∈ X ∧ F x ≤ 1} ∩
                      x⁻¹ • (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                  Type u_2)) :
            ℝ) /
          x ^ card ι) ∘
      fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (↑(card ι) : ℝ)⁻¹)
    fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c
refine_2 :
  Bornology.IsBounded.{u_2} (α := ι → ℝ)
    (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
      {x : E | x ∈ X ∧ F x ≤ 1})
refine_3 :
  MeasurableSet.{u_2} (α := ι → ℝ)
    (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
      {x : E | x ∈ X ∧ F x ≤ 1})
refine_4 :
  ∀ (x y : ℝ) (hx : 0 < x) (hy : x ≤ y),
    HSMul.hSMul (β := Set (ι → ℝ)) x
        (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1}) ⊆
      HSMul.hSMul (β := Set (ι → ℝ)) y
        (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1})
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c) atTop
    (𝓝
      (Measure.real.{u_2} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        (Set.image.{u_1, u_2} (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1})))

Tactic:
refine Tendsto.congr' ?_ <| (tendsto_card_div_pow_atTop_volume'
      ((b.ofZLatticeBasis ℝ).equivFun '' {x ∈ X | F x ≤ 1}) ?_ ?_ h₄ fun x y hx hy ↦ ?_).comp
        (tendsto_rpow_atTop <| inv_pos.mpr
          (Nat.cast_pos.mpr card_pos) : Tendsto (fun x ↦ x ^ (card ι : ℝ)⁻¹) atTop atTop)

Premises used: Iff.mpr, Real, Nat.cast_pos, tendsto_rpow_atTop, setOf, Module.Basis.ofZLatticeBasis, Membership.mem, inv_pos, LE.le, And, Set.image, tendsto_card_div_pow_atTop_volume', Filter.Tendsto.comp, Filter.Tendsto.congr', OfNat.ofNat, DFunLike.coe, Fintype.card_pos, Module.Basis.equivFun