awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c) atTop
    (𝓝
      (Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
        (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1})))

Tactic:
tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_

Premises used: ZLattice.covolume.tendsto_card_le_div''
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  Measure.real.{u_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
      covolume L (volume : Measure E) =
    Measure.real (α := Free.ChooseBasisIndex ℤ ↥L → ℝ) (m := MeasureSpace.toMeasurableSpace) volume
      (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
        {x : E | x ∈ X ∧ F x ≤ 1})
convert_1 : Nonempty.{u_1 + 1} (Free.ChooseBasisIndex ℤ ↥L)
convert_2 : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) * F x
convert_3 :
  Eq (α := ENNReal)
    (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (frontier
          (Set.image (α := E)
            (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
            {x : E | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)
⊢ Tendsto (fun (c : ℝ) ↦ (↑(Nat.card.{u_1} (↑({x : E | x ∈ X ∧ F x ≤ c} ∩ (↑L : Set E)) : Type u_1)) : ℝ) / c) atTop
    (𝓝
      (Measure.real.{u_1} (α := E) (m := MeasureSpace.toMeasurableSpace) volume {x : E | x ∈ X ∧ F x ≤ 1} /
        covolume L (volume : Measure E)))

Tactic:
convert! tendsto_card_le_div'' b hX ?_ h₂ h₃ ?_
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    (HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1} : ENNReal)
        (ENNReal.ofReal (covolume L (volume : Measure E)))).toReal
h₅ :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      (ENNReal.ofReal (covolume L (volume : Measure E))).toReal
h₆ h₇ :
  ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) / covolume L volume
⊢ ENNReal.toReal (((volume : Measure E) : (a : Set E) → ENNReal) {x : E | x ∈ X ∧ F x ≤ 1}) /
      covolume L (volume : Measure E) =
    ENNReal.toReal
      (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (Set.image (α := E) (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
          {x : E | x ∈ X ∧ F x ≤ 1}))

Tactic:
rw [volume_image_eq_volume_div_covolume' L b h₃.nullMeasurableSet, ENNReal.toReal_div,
      ENNReal.toReal_ofReal (covolume_pos L volume).le]

Premises used: MeasurableSet.nullMeasurableSet, LT.lt.le, ENNReal.toReal_ofReal, MeasureTheory.MeasureSpace.volume, ZLattice.volume_image_eq_volume_div_covolume', ZLattice.covolume_pos, ENNReal.toReal_div
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ Nontrivial.{u_1} ↥L

Tactic:
have : Nontrivial L := nontrivial_of_finrank_pos <| (ZLattice.rank ℝ L).symm ▸ finrank_pos
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
this : Nontrivial.{u_1} ↥L
⊢ Nonempty.{u_1 + 1} (Free.ChooseBasisIndex ℤ ↥L)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
convert_2 : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank.{0, u_1} ℤ ↥L * F x
convert_2₁ convert_2₂ convert_2₃ convert_2₄ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
⊢ ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card.{u_1} (Free.ChooseBasisIndex ℤ ↥L) * F x

Tactic:
rwa [← finrank_eq_card_chooseBasisIndex, ZLattice.rank ℝ L]

Premises used: Real, ZLattice.rank, Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
convert_3 : NullMeasurableSet.{u_1} (α := E) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) (volume : Measure E)
⊢ Eq (α := ENNReal)
    (((volume : Measure (Free.ChooseBasisIndex ℤ ↥L → ℝ)) : (a : Set (Free.ChooseBasisIndex ℤ ↥L → ℝ)) → ENNReal)
        (frontier
          (Set.image (α := E)
            (⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → Free.ChooseBasisIndex ℤ ↥L → ℝ)
            {x : E | x ∈ X ∧ F x ≤ 1})) :
      ENNReal)
    (0 : ENNReal)

Tactic:
rw [frontier_equivFun, volume_image_eq_volume_div_covolume', h₄, ENNReal.zero_div]

Premises used: _private.0.ZLattice.covolume.frontier_equivFun, ENNReal.zero_div, ZLattice.volume_image_eq_volume_div_covolume'
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ NullMeasurableSet.{u_1} (α := E) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) (volume : Measure E)

Tactic:
NullMeasurableSet.of_null h₄

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
inst_7 : Nontrivial E
X : Set E
F : E → ℝ
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ finrank ℝ E * F x
h₂ : Bornology.IsBounded.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet.{u_1} (α := E) {x : E | x ∈ X ∧ F x ≤ 1}
h₄ :
  Eq (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) : ENNReal)
    (0 : ENNReal)
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
⊢ NullMeasurableSet.{u_1} (α := E) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) (volume : Measure E)

Tactic:
exact NullMeasurableSet.of_null h₄

Premises used: MeasureTheory.NullMeasurableSet.of_null
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
inr :
  ∀
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
        {L : Submodule ℤ E} [inst_6 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L)
        (H : IsZLattice ℝ L),
        ∃ (ε : ℝ),
          0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖)
    (H : ¬IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
wlog :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_6 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
wlog H : IsZLattice ℝ L

Premises used: Real, IsZLattice
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_6 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
⊢ Continuous (X := ↥E') (Y := E) (⇑E'.subtype : (a : ↥E') → E)

Tactic:
fun_prop
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_6 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
⊢ DiscreteTopology.{u_1} ↥L'

Tactic:
have inst : DiscreteTopology L' :=
      comap_discreteTopology _ _ (by fun_prop) Subtype.val_injective
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_7 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst : DiscreteTopology.{u_1} ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
⊢ Submodule.map E'.subtype (Submodule.span ℝ (↑L' : Set ↥E')) = Submodule.map E'.subtype ⊤

Tactic:
simp [E', L']
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_7 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst : DiscreteTopology.{u_1} ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
⊢ IsZLattice ℝ L'

Tactic:
have inst : IsZLattice ℝ L' :=
      ⟨Submodule.map_injective_of_injective E'.subtype_injective (by simp [E', L'])⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_6 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_8 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst_5 : DiscreteTopology.{u_1} ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
inst : IsZLattice ℝ L'
inr :
  ∀ (ε : ℝ) (hε : 0 < ε)
    (H :
      ∀ (x : ↥L') (i : ι),
        ε * (↑|((((b.map e.symm).repr : (a : ↥L') → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
obtain ⟨ε, hε, H⟩ := this (b.map e.symm) inst

Premises used: LinearEquiv.symm, Module.Basis.map
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_6 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_8 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H_1 : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst_5 : DiscreteTopology.{u_1} ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
inst : IsZLattice ℝ L'
ε : ℝ
hε : 0 < ε
H : ∀ (x : ↥L') (i : ι), ε * (↑|((((b.map e.symm).repr : (a : ↥L') → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
x : ↥L
i : ι
⊢ ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
simpa using H ⟨⟨x.1, Submodule.subset_span x.2⟩, x.2⟩ i

Premises used: Subtype.mk, Submodule.subset_span, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_6 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
    [inst_8 : DiscreteTopology.{u_1} ↥L] {ι : Type u_2} (b : Basis.{u_2, 0, u_1} ι ℤ ↥L) (H : IsZLattice ℝ L),
    ∃ (ε : ℝ),
      0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
H_1 : ¬IsZLattice ℝ L
E' : Submodule ℝ E := Submodule.span ℝ (↑L : Set E)
L' : Submodule ℤ ↥E' := ZLattice.comap ℝ L E'.subtype
inst_5 : DiscreteTopology.{u_1} ↥L'
e : ↥L' ≃ₗ[ℤ] ↥L := Submodule.comapSubtypeEquivOfLe ⋯
inst : IsZLattice ℝ L'
ε : ℝ
hε : 0 < ε
H : ∀ (x : ↥L') (i : ι), ε * (↑|((((b.map e.symm).repr : (a : ↥L') → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
exact ⟨ε, hε, fun x i ↦ by simpa using H ⟨⟨x.1, Submodule.subset_span x.2⟩, x.2⟩ i⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
L_1 : Submodule ℤ E_1
ι_1 : Type u_2
b_1 : Basis.{u_2, 0, u_1} ι_1 ℤ ↥L_1
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
H : IsZLattice ℝ L
⊢ Finite ι

Tactic:
have : Finite ι := Module.Finite.finite_basis b
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
L_1 : Submodule ℤ E_1
ι_1 : Type u_2
b_1 : Basis.{u_2, 0, u_1} ι_1 ℤ ↥L_1
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
H : IsZLattice ℝ L
this : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : ContinuousLinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι → ℝ) :=
  LinearEquiv.toContinuousLinearEquiv (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι)
⊢ IsOpen.{u_1} (X := E)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))

Tactic:
have := e.continuous.1 (Set.univ.pi fun _ ↦ Set.Ioo (-1) 1)
    (isOpen_set_pi Set.finite_univ fun _ _ ↦ isOpen_Ioo)
-- Module: Mathlib.Algebra.Module.ZLattice.Summable
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
L_1 : Submodule ℤ E_1
ι_1 : Type u_2
b_1 : Basis.{u_2, 0, u_1} ι_1 ℤ ↥L_1
E : Type u_1
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
ι : Type u_2
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
H : IsZLattice ℝ L
this_1 : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : ContinuousLinearEquiv.{0, 0, u_1, u_2} (RingHom.id ℝ) E (ι → ℝ) :=
  LinearEquiv.toContinuousLinearEquiv (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι)
this :
  IsOpen.{u_1} (X := E)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
⊢ Membership.mem (γ := Set E)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
    0

Tactic:
simp