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 : 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)
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})
have refine_4 : Subset.{u_2} (α := Set (ι → ℝ))
  ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) ''
    HSMul.hSMul (β := Set E) x {x : E | x ∈ X ∧ F x ≤ 1})
  ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) ''
    HSMul.hSMul (β := Set E) y {x : E | x ∈ X ∧ F x ≤ 1})
Tactic: simp_rw [← image_smul_set]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ Subset.{u_2} (α := Set (ι → ℝ))
    ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) ''
      HSMul.hSMul (β := Set E) x {x : E | x ∈ X ∧ F x ≤ 1})
    ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) ''
      HSMul.hSMul (β := Set E) y {x : E | x ∈ X ∧ F x ≤ 1})
have refine_4 : HSMul.hSMul (β := Set E) x {x : E | x ∈ X ∧ F x ≤ 1} ⊆ HSMul.hSMul (β := Set E) y {x : E | x ∈ X ∧ F x ≤ 1}
Tactic: apply Set.image_mono
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
x y : ℝ
hx : 0 < x
hy : x ≤ y
⊢ HSMul.hSMul (β := Set E) x {x : E | x ∈ X ∧ F x ≤ 1} ⊆ HSMul.hSMul (β := Set E) y {x : E | x ∈ X ∧ F x ≤ 1}
have refine_4 : Subset.{u_1} (α := Set E) {x_1 : E | x_1 ∈ X ∧ F x_1 ≤ x ^ card ι} {x : E | x ∈ X ∧ F x ≤ y ^ card ι}
Tactic: rw [tendsto_card_le_div''_aux hX h₁ hx,
      tendsto_card_le_div''_aux hX h₁ (lt_of_lt_of_le hx hy)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
ι : Type u_2
inst_2 : Finite ι
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : T2Space E
b : Basis ι ℝ E
s : Set E
⊢ Eq.{u_2 + 1} (α := Set (ι → ℝ)) (frontier ((⇑b.equivFun : (a : E) → ι → ℝ) '' s))
    ((⇑b.equivFun : (a : E) → ι → ℝ) '' frontier s)
have rw : Eq.{u_2 + 1} (α := Set (ι → ℝ)) (frontier ((⇑b.equivFun.symm : (a : ι → ℝ) → E) ⁻¹' s))
  ((⇑b.equivFun.symm : (a : ι → ℝ) → E) ⁻¹' frontier s)
Tactic: rw [LinearEquiv.image_eq_preimage_symm, LinearEquiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
⊢ 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 (ι → ℝ))))
have 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)
Tactic: convert! tendsto_card_div_pow'' b hs₁ hs₂ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
⊢ 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 (ι → ℝ))))
have convert! : Eq (α := ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' 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:
ι : 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)
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s))
have h : ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
    covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
  (HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))).toReal
Tactic: rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 :
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    (HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
        (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))).toReal
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s))
have h₁ : ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
    covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
    (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)))).toReal
Tactic: rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 :
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    (HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
        (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))).toReal
h₁ :
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)))).toReal
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
      covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    ENNReal.toReal
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s))
have h₂ : ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) /
    covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
  ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s) / covolume.{u_1} (E := ι → ℝ) L volume
Tactic: rw [volume_image_eq_volume_div_covolume L b, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
have rw : Eq (α := ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b) : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) : (a : ι → ℝ) → ι → ℝ) '' frontier s) :
    ENNReal)
  (0 : ENNReal)
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:
ι : 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)
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
have rw₁ : HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal)
    (ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ)))) =
  0
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:
ι : 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
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
have rw₂ : 0 / ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))) = 0
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:
ι : 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
⊢ Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
have rw₃ : Eq (α := ENNReal) 0 0
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:
ι : 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)
⊢ 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 (ι → ℝ))))
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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)
⊢ 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 (ι → ℝ))))
have convert! : Eq (α := ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s)) :
    ENNReal)
  (0 : ENNReal)
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 ι
⊢ Free.ChooseBasisIndex ℤ ↥L ≃ ι
have refine : card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = card ι
Tactic: refine Fintype.equivOfCardEq ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 ι
⊢ card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = card ι
have rw : finrank.{0, u_1} ℤ ↥L = card ι
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 ι
⊢ card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = card ι
have rw₁ : finrank.{0, u_1} ℝ (ι → ℝ) = card ι
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 ι
⊢ card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) = card ι
have rw₂ : card ι = card ι
Tactic: rw [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ, finrank_fintype_fun_eq_card]