awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
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 {x : ι → ℝ | x ∈ X ∧ F x ≤ 1} /
        covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
have 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})
Tactic: convert! tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_
-- 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 ι
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})
⊢ 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 (ι → ℝ))))
have 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)
Tactic: convert! tendsto_card_le_div'' b hX h₁ h₂ h₃ ?_
-- 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 ι
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq ⋯
b : Basis ι ℤ ↥L := Basis.reindex (Free.chooseBasis ℤ ↥L) e
⊢ 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}))
have 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
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
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
⊢ 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}))
have 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
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
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
⊢ 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}))
have 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
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
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
⊢ 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)
have 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)
Tactic: rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, 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 ι
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)
⊢ 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)
have 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
Tactic: rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, 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 ι
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
⊢ 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)
have rw₂ : 0 / ENNReal.ofReal (covolume.{u_1} (E := ι → ℝ) L (volume : Measure (ι → ℝ))) = 0
Tactic: rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, 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 ι
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
⊢ 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)
have rw₃ : Eq (α := ENNReal) 0 0
Tactic: rw [frontier_equivFun, volume_image_eq_volume_div_covolume, h₄, 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 ι
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 (ι → ℝ))))
⊢ 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 (ι → ℝ))))
have h : let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq sorry;
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})
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]
-- 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 ι
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})
⊢ 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 (ι → ℝ))))
have let₄ : let e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := equivOfCardEq sorry;
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)
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]
-- 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
⊢ 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 h : ∀ (x : ℕ), finrank ℝ E = Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)
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
h : ∀ (x : ℕ), finrank ℝ E = Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L)
⊢ 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 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)
Tactic: convert! tendsto_card_div_pow'' b hs₁ hs₂ ?_