awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
rw :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) '' frontier s) :
      ENNReal)
    (0 : ENNReal)
rw₁ :
  HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal)
      (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)))) =
    0
rw₂ : 0 / ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))) = 0
rw₃ rw₄ : Eq (α := ENNReal) 0 0
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)

Tactic:
rw [frontier_equivFun, volume_image_eq_volume_div_covolume, hs₃, ENNReal.zero_div]

Premises used: _private.0.ZLattice.covolume.frontier_equivFun, ENNReal.zero_div, ZLattice.volume_image_eq_volume_div_covolume
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
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 /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    Measure.real (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)
convert! convert!₁ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set (ι → ℝ))) : Type u_1)) : ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s /
        covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))

Tactic:
classical
  convert! tendsto_card_div_pow'' b hs₁ hs₂ ?_
  · simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume, hs₃, ENNReal.zero_div]

Premises used: _private.0.ZLattice.covolume.frontier_equivFun, ENNReal.zero_div, LT.lt.le, ENNReal.toReal_ofReal, ZLattice.volume_image_eq_volume_div_covolume, MeasureTheory.MeasureSpace.volume, ZLattice.covolume_pos, MeasureTheory.measureReal_def, ENNReal.toReal_div, ZLattice.covolume.tendsto_card_div_pow''
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
refine : card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = card ι
⊢ Free.ChooseBasisIndex ℤ ↥L ≃ ι

Tactic:
refine Fintype.equivOfCardEq ?_

Premises used: Fintype.equivOfCardEq
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
rw : finrank.{0, u_1} ℤ ↥L = card ι
rw₁ : finrank.{0, u_1} ℝ (ι → ℝ) = card ι
rw₂ rw₃ : card ι = card ι
⊢ card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = card ι

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]

Premises used: Real, ZLattice.rank, Module.finrank_eq_card_chooseBasisIndex, Module.finrank_fintype_fun_eq_card
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := Basis.reindex (Free.chooseBasis ℤ ↥L) e
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : ι → ℝ | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set (ι → ℝ))) : Type u_1)) : ℝ) / c)
    atTop
    (𝓝
      (Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
          {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})))

Tactic:
tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_

Premises used: ZLattice.covolume.tendsto_card_le_div''
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := Basis.reindex (Free.chooseBasis ℤ ↥L) e
h :
  Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
        {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})
convert! :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier
          (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
            {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : ι → ℝ | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set (ι → ℝ))) : Type u_1)) : ℝ) / c)
    atTop
    (𝓝
      (Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} /
        covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))

Tactic:
convert! tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_

Premises used: ZLattice.covolume.tendsto_card_le_div''
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := Basis.reindex (Free.chooseBasis ℤ ↥L) e
h :
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    (HDiv.hDiv (α := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} : ENNReal)
        (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))).toReal
h₅ :
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) /
      (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)))).toReal
h₆ h₇ :
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) /
      covolume.{u_1} (E := ι → ℝ) L volume
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
          {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}))

Tactic:
rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]

Premises used: LT.lt.le, ENNReal.toReal_ofReal, ZLattice.volume_image_eq_volume_div_covolume, MeasureTheory.MeasureSpace.volume, ZLattice.covolume_pos, ENNReal.toReal_div
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := Basis.reindex (Free.chooseBasis ℤ ↥L) e
rw :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (Set.image (α := ι → ℝ)
          (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ)
          (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)
rw₁ :
  HDiv.hDiv (α := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
      (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)))) =
    0
rw₂ : 0 / ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))) = 0
rw₃ rw₄ : Eq (α := ENNReal) 0 0
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier
          (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
            {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)

Tactic:
rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, ENNReal.zero_div]

Premises used: _private.0.ZLattice.covolume.frontier_equivFun, ENNReal.zero_div, ZLattice.volume_image_eq_volume_div_covolume
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_1
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_1} ↥L
inst_2 : IsZLattice.{0, u_1} ℝ (E := ι → ℝ) L
X : Set (ι → ℝ)
hX : ∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : (ι → ℝ) → ℝ
h₁ : ∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := ι → ℝ) {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier {x : ι → ℝ | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
inst_3 : Nonempty ι
let let₁ let₂ let₃ :
  Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : ι → ℝ | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set (ι → ℝ))) : Type u_1)) : ℝ) / c)
    atTop
    (𝓝
      (Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} /
        covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
h :
  let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯;
  let b := Basis.reindex (Free.chooseBasis ℤ ↥L) e;
  Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
        {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})
let₄ let₅ :
  let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯;
  let b := Basis.reindex (Free.chooseBasis ℤ ↥L) e;
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier
          (Set.image (α := ι → ℝ) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ)
            {x : ι → ℝ | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : ι → ℝ | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set (ι → ℝ))) : Type u_1)) : ℝ) / c)
    atTop
    (𝓝
      (Measure.real.{u_1} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} /
        covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))

Tactic:
classical
  let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := by
    refine Fintype.equivOfCardEq ?_
    rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
  let b := (Module.Free.chooseBasis ℤ L).reindex e
  convert! tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_
  · simp only [measureReal_def]
    rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
  · rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, ENNReal.zero_div]

Premises used: _private.0.ZLattice.covolume.frontier_equivFun, ENNReal.zero_div, LT.lt.le, ENNReal.toReal_ofReal, ZLattice.volume_image_eq_volume_div_covolume, MeasureTheory.MeasureSpace.volume, ZLattice.covolume_pos, MeasureTheory.measureReal_def, ENNReal.toReal_div
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)))
    atTop
    (𝓝
      (Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ) '' s)))

Tactic:
tendsto_card_div_pow'' b hs₁ hs₂ ?_

Premises used: ZLattice.covolume.tendsto_card_div_pow''
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h : ∀ (x : ℕ), finrank ℝ E = Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)
h₁ :
  Measure.real (m := MeasureSpace.toMeasurableSpace) volume s / covolume L (volume : Measure E) =
    Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ) '' s)
convert! :
  Eq (α := ENNReal)
    (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (finrank ℝ E))
    atTop (𝓝 (Measure.real (m := MeasureSpace.toMeasurableSpace) volume s / covolume L (volume : Measure E)))

Tactic:
convert! tendsto_card_div_pow'' b hs₁ hs₂ ?_

Premises used: ZLattice.covolume.tendsto_card_div_pow''
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : ℕ
h : finrank ℝ E = finrank.{0, u_1} ℤ ↥L
h₁ h₂ : finrank ℝ E = finrank ℝ E
⊢ finrank ℝ E = Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)

Tactic:
rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]

Premises used: Real, ZLattice.rank, Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) s) / covolume L (volume : Measure E) =
    (HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
        (ENNReal.ofReal (covolume L (volume : Measure E)))).toReal
h₁ :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) s) / covolume L (volume : Measure E) =
    ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) s) /
      (ENNReal.ofReal (covolume L (volume : Measure E))).toReal
h₂ h₃ :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) s) / covolume L (volume : Measure E) =
    ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) s) / covolume L volume
⊢ ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) s) / covolume L (volume : Measure E) =
    ENNReal.toReal
      (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ) '' s))

Tactic:
rw [volume_image_eq_volume_div_covolume' L b hs₂.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]

Premises used: MeasurableSet.nullMeasurableSet, LT.lt.le, ENNReal.toReal_ofReal, MeasureTheory.MeasureSpace.volume, ZLattice.volume_image_eq_volume_div_covolume', ZLattice.covolume_pos, ENNReal.toReal_div
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
hs : NullMeasurableSet (frontier s) (volume : Measure E)
⊢ Eq (α := ENNReal)
    (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)

Tactic:
rw [frontier_equivFun, volume_image_eq_volume_div_covolume', hs₃, ENNReal.zero_div]

Premises used: _private.0.ZLattice.covolume.frontier_equivFun, ENNReal.zero_div, ZLattice.volume_image_eq_volume_div_covolume'
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ NullMeasurableSet (frontier s) (volume : Measure E)

Tactic:
NullMeasurableSet.of_null hs₃

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ NullMeasurableSet (frontier s) (volume : Measure E)

Tactic:
exact NullMeasurableSet.of_null hs₃

Premises used: MeasureTheory.NullMeasurableSet.of_null