awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_2
inst : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L₁
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L₁
inst_3 : DiscreteTopology.{u_2} ↥L₂
inst_4 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
i j : ι
⊢ Eq (α := ℝ)
    (((((Basis.repr (Basis.ofZLatticeBasis ℝ L₂ b₂) : (ι → ℝ) ≃ₗ[ℝ] ι →₀ ℝ) : (a : ι → ℝ) → ι →₀ ℝ)
              (↑((b₁ : (a : ι) → ↥L₁) j) : ι → ℝ) :
            ι →₀ ℝ) :
          (a : ι) → ℝ)
        i :
      ℝ)
    ((↑((((b₂.repr :
                    (a :
                        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                            L₂.toAddSubgroup)) →
                      ι →₀ ℤ)
                  (Subtype.mk (p := fun (x : ι → ℝ) ↦
                    Membership.mem (γ := Submodule ℤ (ι → ℝ))
                      ((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ)) L₂.toAddSubgroup :
                        Submodule ℤ (ι → ℝ))
                      x)
                    (↑((b₁ :
                            (a : ι) →
                              ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                                  L₁.toAddSubgroup))
                          j) :
                      ι → ℝ)
                    ⋯) :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        ℝ) :
      ℝ)

Tactic:
(b₂.ofZLatticeBasis_repr_apply ℝ L₂ ⟨b₁ j, h (coe_mem _)⟩ i)

Premises used: Real, Set.Mem, Submodule.coe_mem, Subtype.mk, Module.Basis.ofZLatticeBasis_repr_apply, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
ι : Type u_2
inst : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L₁
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L₁
inst_3 : DiscreteTopology.{u_2} ↥L₂
inst_4 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L₂
h : L₁ ≤ L₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
i j : ι
⊢ Eq (α := ℝ)
    (((((Basis.repr (Basis.ofZLatticeBasis ℝ L₂ b₂) : (ι → ℝ) ≃ₗ[ℝ] ι →₀ ℝ) : (a : ι → ℝ) → ι →₀ ℝ)
              (↑((b₁ : (a : ι) → ↥L₁) j) : ι → ℝ) :
            ι →₀ ℝ) :
          (a : ι) → ℝ)
        i :
      ℝ)
    ((↑((((b₂.repr :
                    (a :
                        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                            L₂.toAddSubgroup)) →
                      ι →₀ ℤ)
                  (Subtype.mk (p := fun (x : ι → ℝ) ↦
                    Membership.mem (γ := Submodule ℤ (ι → ℝ))
                      ((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ)) L₂.toAddSubgroup :
                        Submodule ℤ (ι → ℝ))
                      x)
                    (↑((b₁ :
                            (a : ι) →
                              ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                                  L₁.toAddSubgroup))
                          j) :
                      ι → ℝ)
                    ⋯) :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        ℝ) :
      ℝ)

Tactic:
exact (b₂.ofZLatticeBasis_repr_apply ℝ L₂ ⟨b₁ j, h (coe_mem _)⟩ i)

Premises used: Real, Submodule.coe_mem, Subtype.mk, Module.Basis.ofZLatticeBasis_repr_apply, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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₁ L₂ : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L₁
inst_6 : IsZLattice ℝ L₁
inst_7 : DiscreteTopology.{u_2} ↥L₂
inst_8 : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ))
    (ContinuousLinearEquiv.symm
      (↑(OrthonormalBasis.repr (stdOrthonormalBasis ℝ E)) : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))))
⊢ MeasurePreserving (α := Fin (finrank ℝ E) → ℝ) (β := E) (⇑f : (a : Fin (finrank ℝ E) → ℝ) → E) volume
    (volume : Measure E)

Tactic:
have hf : MeasurePreserving f := (stdOrthonormalBasis ℝ E).measurePreserving_repr_symm.comp
    (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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 ι
rw₁ rw₂ : Fintype.card ι = Fintype.card ι
⊢ Fintype.card (Fin (finrank ℝ E)) = Fintype.card ι

Tactic:
rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)]

Premises used: Real, Fintype.card_fin, Module.Basis.ofZLatticeBasis, Module.finrank_eq_card_basis
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)
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)
⊢ ((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:
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]

Premises used: Real, ContinuousLinearEquiv.toLinearEquiv, ZLattice.comap, ContinuousLinearEquiv.image_symm_eq_preimage, ZLattice.volume_image_eq_volume_div_covolume, LinearEquiv.toLinearMap, MeasureTheory.MeasureSpace.volume, Module.Basis.ofZLatticeComap, Set.image_comp, ZLattice.covolume_comap, Module.Basis.ofZLatticeBasis_comap, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)
⊢ 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:
simp
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)))

Tactic:
Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)

Premises used: Real, tendsto_card_div_pow_atTop_volume, Module.Basis.ofZLatticeBasis, Set.image, Filter.Tendsto.congr', DFunLike.coe, Module.Basis.equivFun
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)
refine_3 : MeasurableSet.{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)))

Tactic:
refine Tendsto.congr' ?_
    (tendsto_card_div_pow_atTop_volume ((b.ofZLatticeBasis ℝ).equivFun '' s) ?_ ?_ hs₃)

Premises used: Real, tendsto_card_div_pow_atTop_volume, Module.Basis.ofZLatticeBasis, Set.image, Filter.Tendsto.congr', DFunLike.coe, Module.Basis.equivFun
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)
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 ι)
⊢ 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:
filter_upwards [eventually_gt_atTop 0] with n hn

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
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)
⊢ (↑(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:
congr
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)

Tactic:
Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm

Premises used: Real, Module.Basis.ofZLatticeBasis, Equiv.subtypeEquiv, Nat.card_congr, LinearEquiv.toEquiv, Equiv.symm, Module.Basis.equivFun
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
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 :
          ι → ℝ)
⊢ 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:
refine Nat.card_congr <| ((b.ofZLatticeBasis ℝ).equivFun.toEquiv.subtypeEquiv fun x ↦ ?_).symm

Premises used: Real, Module.Basis.ofZLatticeBasis, Equiv.subtypeEquiv, Nat.card_congr, LinearEquiv.toEquiv, Equiv.symm, Module.Basis.equivFun
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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_2 :
  ∀ (hs₁ : IsVonNBounded ℝ 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)),
    IsVonNBounded.{0, u_2} ℝ (E := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)
⊢ Bornology.IsBounded.{u_2} (α := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)

Tactic:
rw [← NormedSpace.isVonNBounded_iff ℝ] at hs₁ ⊢

Premises used: Real, NormedSpace.isVonNBounded_iff
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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₁ : IsVonNBounded ℝ 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)
⊢ IsVonNBounded.{0, u_2} ℝ (E := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)

Tactic:
Bornology.IsVonNBounded.image hs₁ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)

Premises used: Real, Module.Basis.equivFunL, Module.Basis.ofZLatticeBasis, Bornology.IsVonNBounded.image, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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₁ : IsVonNBounded ℝ 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)
⊢ IsVonNBounded.{0, u_2} ℝ (E := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)

Tactic:
exact Bornology.IsVonNBounded.image hs₁ ((b.ofZLatticeBasis ℝ).equivFunL : E →L[ℝ] ι → ℝ)

Premises used: Real, Module.Basis.equivFunL, Module.Basis.ofZLatticeBasis, Bornology.IsVonNBounded.image, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)
⊢ MeasurableSet.{u_2} (α := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)

Tactic:
(b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hs₂

Premises used: Iff.mpr, Real, Module.Basis.equivFunL, Module.Basis.ofZLatticeBasis, MeasurableEquiv.measurableSet_image, Homeomorph.toMeasurableEquiv, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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)
⊢ MeasurableSet.{u_2} (α := ι → ℝ) ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s)

Tactic:
exact (b.ofZLatticeBasis ℝ).equivFunL.toHomeomorph.toMeasurableEquiv.measurableSet_image.mpr hs₂

Premises used: Iff.mpr, Real, Module.Basis.equivFunL, Module.Basis.ofZLatticeBasis, MeasurableEquiv.measurableSet_image, Homeomorph.toMeasurableEquiv, ContinuousLinearEquiv.toHomeomorph
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
h :
  ∀ (x : E),
    x ∈ HSMul.hSMul (β := Set E) c {x : E | x ∈ X ∧ F x ≤ 1} ↔
      Membership.mem (γ := Set E) {x : E | x ∈ X ∧ F x ≤ c ^ card ι} x
⊢ HSMul.hSMul (β := Set E) c {x : E | x ∈ X ∧ F x ≤ 1} = {x : E | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
ext x