awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
rw :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) : (a : ι → ℝ) → ι → ℝ) ⁻¹' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
have rw₁ : HMul.hMul (β := ENNReal)
    (ENNReal.ofReal
      |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
          (↑(LinearEquiv.symm (LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)))) :
            (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
  HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
    (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
Tactic: rw [LinearEquiv.image_eq_preimage_symm, Measure.addHaar_preimage_linearEquiv,
    LinearEquiv.symm_symm, covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul,
    ENNReal.ofReal_inv_of_pos (abs_pos.2 (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
rw :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) : (a : ι → ℝ) → ι → ℝ) ⁻¹' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
rw₁ :
  HMul.hMul (β := ENNReal)
      (ENNReal.ofReal
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            (↑(LinearEquiv.symm (LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)))) :
              (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
have rw₂ : HMul.hMul (β := ENNReal)
    (ENNReal.ofReal
      |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
          (↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
  HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
    (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
Tactic: rw [LinearEquiv.image_eq_preimage_symm, Measure.addHaar_preimage_linearEquiv,
    LinearEquiv.symm_symm, covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul,
    ENNReal.ofReal_inv_of_pos (abs_pos.2 (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
rw :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) : (a : ι → ℝ) → ι → ℝ) ⁻¹' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
rw₁ :
  HMul.hMul (β := ENNReal)
      (ENNReal.ofReal
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            (↑(LinearEquiv.symm (LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)))) :
              (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
rw₂ :
  HMul.hMul (β := ENNReal)
      (ENNReal.ofReal
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            (↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
have rw₃ : HMul.hMul (β := ENNReal)
    (ENNReal.ofReal
      |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
          (↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
  HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
    (ENNReal.ofReal
      |(↑(((LinearEquiv.det : ((ι → ℝ) ≃ₗ[ℝ] ι → ℝ) →* ℝˣ) : (a : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) → ℝˣ)
                (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) :
            ℝ)|⁻¹)
Tactic: rw [LinearEquiv.image_eq_preimage_symm, Measure.addHaar_preimage_linearEquiv,
    LinearEquiv.symm_symm, covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul,
    ENNReal.ofReal_inv_of_pos (abs_pos.2 (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_2
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_2} ↥L
inst_6 : IsZLattice ℝ L
ι : Type u_3
inst_7 : Fintype ι
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s (volume : Measure E)
⊢ Fintype.card (Fin (finrank ℝ E)) = Fintype.card ι
have rw : finrank ℝ E = Fintype.card ι
Tactic: rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_2
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_2} ↥L
inst_6 : IsZLattice ℝ L
ι : Type u_3
inst_7 : Fintype ι
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s (volume : Measure E)
rw : finrank ℝ E = Fintype.card ι
⊢ Fintype.card (Fin (finrank ℝ E)) = Fintype.card ι
have rw₁ : Fintype.card ι = Fintype.card ι
Tactic: rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_2
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_2} ↥L
inst_6 : IsZLattice ℝ L
ι : Type u_3
inst_7 : Fintype ι
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s (volume : Measure E)
e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯
f : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (ι → ℝ) E :=
  (ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)).trans
    (ContinuousLinearEquiv.symm
      (↑(OrthonormalBasis.repr (OrthonormalBasis.reindex (stdOrthonormalBasis ℝ E) e)) : E ≃L[ℝ] EuclideanSpace ℝ ι))
hf :
  MeasurePreserving.{u_3, u_2} (α := ι → ℝ) (β := E) (⇑f : (a : ι → ℝ) → E) (volume : Measure (ι → ℝ))
    (volume : Measure E)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))
have rw : Eq (α := ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) :
    ENNReal)
  (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      (Function.comp (β := ι → ℝ)
          (⇑(Basis.map (Basis.ofZLatticeBasis ℝ L b) (↑f.symm : E ≃ₗ[ℝ] ι → ℝ)).equivFun : (a : ι → ℝ) → ι → ℝ)
          (⇑f.symm : (a : E) → ι → ℝ) ''
        s) :
    ENNReal)
Tactic: rw [← hf.measure_preimage hs, ← (covolume_comap L volume volume hf),
    ← volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap)
    (b.ofZLatticeComap ℝ L f.toLinearEquiv), Basis.ofZLatticeBasis_comap,
    ← f.image_symm_eq_preimage, ← Set.image_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_2
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_2} ↥L
inst_6 : IsZLattice ℝ L
ι : Type u_3
inst_7 : Fintype ι
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s (volume : Measure E)
let let₁ let₂ let₃ :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))
have let₄ : let e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq sorry;
let f : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (ι → ℝ) E :=
  (ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)).trans
    (ContinuousLinearEquiv.symm
      (↑(OrthonormalBasis.repr (OrthonormalBasis.reindex (stdOrthonormalBasis ℝ E) e)) : E ≃L[ℝ] EuclideanSpace ℝ ι));
∀
  (hf :
    MeasurePreserving.{u_3, u_2} (α := ι → ℝ) (β := E) (⇑f : (a : ι → ℝ) → E) (volume : Measure (ι → ℝ))
      (volume : Measure E)),
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))
Tactic: classical
  let e : Fin (finrank ℝ E) ≃ ι :=
    Fintype.equivOfCardEq (by rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)])
  let f := (EuclideanSpace.equiv ι ℝ).symm.trans
    ((stdOrthonormalBasis ℝ E).reindex e).repr.toContinuousLinearEquiv.symm
  have hf : MeasurePreserving f :=
    ((stdOrthonormalBasis ℝ E).reindex e).measurePreserving_repr_symm.comp
      (PiLp.volume_preserving_toLp ι)
  rw [← hf.measure_preimage hs, ← (covolume_comap L volume volume hf),
    ← volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap)
    (b.ofZLatticeComap ℝ L f.toLinearEquiv), Basis.ofZLatticeBasis_comap,
    ← f.image_symm_eq_preimage, ← Set.image_comp]
  simp
-- 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (Measure.real.{u_2} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)))
have refine_1 : EventuallyEq (β := ℝ) atTop
  (fun (n : ℕ) ↦
    (↑(Nat.card.{u_2}
            (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_2)) :
        ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
  fun (n : ℕ) ↦
  (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
    HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
Tactic: refine Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
-- 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
refine_1 :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_2}
              (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_2)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    fun (n : ℕ) ↦
    (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (Measure.real.{u_2} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)))
have refine_2 : Bornology.IsBounded.{u_2} (α := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
Tactic: refine Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
-- 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
refine_1 :
  EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_2}
              (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_2)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    fun (n : ℕ) ↦
    (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
refine_2 :
  Bornology.IsBounded.{u_2} (α := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (Measure.real.{u_2} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)))
have refine_3 : MeasurableSet.{u_2} (α := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
Tactic: refine Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)
-- 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
⊢ EventuallyEq (β := ℝ) atTop
    (fun (n : ℕ) ↦
      (↑(Nat.card.{u_2}
              (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_2)) :
          ℝ) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    fun (n : ℕ) ↦
    (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
have h : ∀ (n : ℕ) (hn : 0 < n),
  (↑(Nat.card.{u_2}
            (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_2)) :
        ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι) =
    (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
Tactic: filter_upwards [eventually_gt_atTop 0] with n hn
-- 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
n : ℕ
hn : 0 < n
⊢ (↑(Nat.card.{u_2}
            (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
                  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
              Type u_2)) :
        ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι) =
    (↑(Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)) : ℝ) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
have h : Nat.card.{u_2}
    (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_2) =
  Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)
Tactic: congr
-- 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
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        (frontier ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)) :
      ENNReal)
    (0 : ENNReal)
n : ℕ
hn : 0 < n
⊢ Nat.card.{u_2}
      (↑((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_2) =
    Nat.card.{u_1} (↑(s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E)) : Type u_1)
have h : ∀ (x : E),
  x ∈ s ∩ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (↑L : Set E) ↔
    Membership.mem (α := ι → ℝ)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)))
      ((LinearEquiv.toEquiv (modM := NormedSpace.toModule) (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) :
            (a : E) → ι → ℝ)
          x :
        ι → ℝ)
Tactic: refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm