awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
⊢ 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)))
have 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)
Tactic: convert! tendsto_card_div_pow'' b hs₁ hs₂ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 : ℕ
⊢ finrank ℝ E = Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)
have h : finrank ℝ E = finrank.{0, u_1} ℤ ↥L
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
⊢ finrank ℝ E = Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)
have h₁ : finrank ℝ E = finrank ℝ E
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
⊢ 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))
have 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
Tactic: rw [volume_image_eq_volume_div_covolume' L b hs₂.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
⊢ 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))
have 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
Tactic: rw [volume_image_eq_volume_div_covolume' L b hs₂.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
⊢ 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))
have 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
Tactic: rw [volume_image_eq_volume_div_covolume' L b hs₂.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
⊢ 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)
have hs : NullMeasurableSet (frontier s) (volume : Measure E)
Tactic: rw [frontier_equivFun, volume_image_eq_volume_div_covolume', hs₃, ENNReal.zero_div]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ 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_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
        covolume L (volume : Measure E)))
have h : Measure.real.{u_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
    covolume L (volume : Measure E) =
  Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
    (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
      {x : E | x ∈ X ∧ F x ≤ 1})
Tactic: convert! tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  Measure.real.{u_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
      covolume L (volume : Measure E) =
    Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
        {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_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
        covolume L (volume : Measure E)))
have convert_1 : Nonempty.{u_1 + 1} (Free.ChooseBasisIndex ℤ ↥L)
Tactic: convert! tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  Measure.real.{u_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
      covolume L (volume : Measure E) =
    Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
        {x : E | x ∈ X ∧ F x ≤ 1})
convert_1 : Nonempty.{u_1 + 1} (Free.ChooseBasisIndex ℤ ↥L)
⊢ 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_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
        covolume L (volume : Measure E)))
have convert_2 : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) * F x
Tactic: convert! tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  Measure.real.{u_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
      covolume L (volume : Measure E) =
    Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
        {x : E | x ∈ X ∧ F x ≤ 1})
convert_1 : Nonempty.{u_1 + 1} (Free.ChooseBasisIndex ℤ ↥L)
convert_2 : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) * F x
⊢ 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_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
        covolume L (volume : Measure E)))
have convert_3 : Eq (α := ENNReal)
  (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
      (frontier
        (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1})) :
    ENNReal)
  (0 : ENNReal)
Tactic: convert! tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal
      (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1}))
have h : ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
    covolume L (volume : Measure E) =
  (HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1} : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))).toReal
Tactic: rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    (HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1} : ENNReal)
        (ENNReal.ofReal (covolume L (volume : Measure E)))).toReal
⊢ ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal
      (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1}))
have h₅ : ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
    covolume L (volume : Measure E) =
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
    (ENNReal.ofReal (covolume L (volume : Measure E))).toReal
Tactic: rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    (HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1} : ENNReal)
        (ENNReal.ofReal (covolume L (volume : Measure E)))).toReal
h₅ :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      (ENNReal.ofReal (covolume L (volume : Measure E))).toReal
⊢ ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal
      (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1}))
have h₆ : ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
    covolume L (volume : Measure E) =
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) / covolume L volume
Tactic: rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Nonempty.{u_1 + 1} (Free.ChooseBasisIndex ℤ ↥L)
have this : Nontrivial.{u_1} ↥L
Tactic: have : Nontrivial L := nontrivial_of_finrank_pos <| (ZLattice.rank ℝ L).symm ▸ finrank_pos
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * 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 E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) * F x
have convert_2 : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank.{0, u_1} ℤ ↥L * F x
Tactic: rwa [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]