awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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
⊢ 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)
have convert_3 : NullMeasurableSet.{u_1} (α := E) (frontier {x : E | x ∈ X ∧ F x ≤ 1}) (volume : Measure E)
Tactic: rw [frontier_equivFun, volume_image_eq_volume_div_covolume', h₄, ENNReal.zero_div]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have 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‖
Tactic: wlog H : IsZLattice ℝ L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have 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‖
Tactic: wlog H : IsZLattice ℝ L
Cleared hypotheses: inst_1, inst_2, inst_3
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have inst : DiscreteTopology.{u_1} ↥L'
Tactic: have inst : DiscreteTopology L' :=
      comap_discreteTopology _ _ (by fun_prop) Subtype.val_injective
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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 ⋯
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have inst₁ : IsZLattice ℝ L'
Tactic: have inst : IsZLattice ℝ L' :=
      ⟨Submodule.map_injective_of_injective E'.subtype_injective (by simp [E', L'])⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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'
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have 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‖
Tactic: obtain ⟨ε, hε, H⟩ := this (b.map e.symm) inst
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have this : Finite ι
Tactic: have : Finite ι := Module.Finite.finite_basis b
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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 ℝ ℝ ι)
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have 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))
Tactic: have := e.continuous.1 (Set.univ.pi fun _ ↦ Set.Ioo (-1) 1)
    (isOpen_set_pi Set.finite_univ fun _ _ ↦ isOpen_Ioo)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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))
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have obtain : ∀ (ε : ℝ) (hε : ε > 0)
  (hε' :
    Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
      (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
        (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))),
  ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
Tactic: obtain ⟨ε, hε, hε'⟩ := Metric.isOpen_iff.mp this 0 (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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))
ε : ℝ
hε : ε > 0
hε' :
  Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have refine : ∀ (x : ↥L) (i : ι), ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
Tactic: refine ⟨ε / 2, by positivity, fun x i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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))
ε : ℝ
hε : ε > 0
hε' :
  Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
x : ↥L
i : ι
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have pos : ∀ (hx : x = 0), ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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))
ε : ℝ
hε : ε > 0
hε' :
  Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
x : ↥L
i : ι
pos : ∀ (hx : x = 0), ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have neg : ∀ (hx : ¬x = 0), ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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))
ε : ℝ
hε : ε > 0
hε' :
  Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
x : ↥L
i : ι
hx : ¬x = 0
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have hx₁ : ‖(↑x : E)‖ ≠ 0
Tactic: have hx : ‖x.1‖ ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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))
ε : ℝ
hε : ε > 0
hε' :
  Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
x : ↥L
i : ι
hx_1 : ¬x = 0
hx : ‖(↑x : E)‖ ≠ 0
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have this₁ : |ε / 2 * (‖x‖⁻¹ * (↑((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i) : ℝ))| < 1
Tactic: have : |ε / 2 * (‖↑x‖⁻¹ * (b.repr x) i)| < 1 := by
    simpa [e, b', ← abs_lt] using @hε' ((ε / 2) • ‖x‖⁻¹ • x)
      (by simpa [norm_smul, inv_mul_cancel₀ hx, abs_eq_self.mpr hε.le]) i trivial
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
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_2 :
  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))
ε : ℝ
hε : ε > 0
hε' :
  Subset.{u_1} (α := Set E) (Metric.ball 0 ε)
    (Set.preimage.{u_1, u_2} (β := ι → ℝ) (⇑e : (a : E) → ι → ℝ)
      (Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ioo (-1) 1))
x : ↥L
i : ι
hx_1 : ¬x = 0
hx : ‖(↑x : E)‖ ≠ 0
this : |ε / 2 * (‖x‖⁻¹ * (↑((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i) : ℝ))| < 1
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
have this₁ : ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) < ‖x‖
Tactic: rw [abs_mul, abs_mul, abs_inv, mul_left_comm, abs_norm, inv_mul_lt_iff₀ (by positivity),
    mul_one, abs_eq_self.mpr (by positivity), ← Int.cast_abs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
i : ι
⊢ (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ (normBound b)⁻¹ * ‖x‖
have rw : normBound b * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
Tactic: rw [le_inv_mul_iff₀ (normBound_pos b)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
hxn : ‖x‖ < normBound b * (↑n : ℝ)
i : ι
⊢ LT.lt (α := ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ) ((↑n : ℤ) : ℤ)
have refine : (normBound b)⁻¹ * ‖x‖ < (↑(↑n : ℤ) : ℝ)
Tactic: refine Int.cast_lt.mp ((abs_repr_le b x i).trans_lt ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
hxn : ‖x‖ < normBound b * (↑n : ℝ)
i : ι
⊢ (normBound b)⁻¹ * ‖x‖ < (↑(↑n : ℤ) : ℝ)
have rwa : ‖x‖ < normBound b * (↑(↑n : ℤ) : ℝ)
Tactic: rwa [inv_mul_lt_iff₀ (normBound_pos b)]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
i : ι
hi : LE.le (α := ℤ) ((↑n : ℤ) : ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ)
⊢ normBound b * (↑n : ℝ) ≤ ‖x‖
have contrapose! : ∀ (hi : ‖x‖ < normBound b * (↑n : ℝ)),
  LT.lt (α := ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ) ((↑n : ℤ) : ℤ)
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
d : ℕ
hd : d = Fintype.card ι
n : ℕ
r : ℝ
hr : r < -(↑d : ℝ)
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
⊢ ∑ p ∈ Fintype.piFinset (δ := fun (x : ι) ↦ ℤ) fun (x : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * normBound b ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have subst : ∀ (hr : r < -(↑(Fintype.card ι) : ℝ)),
  ∑ p ∈ Fintype.piFinset (δ := fun (x : ι) ↦ ℤ) fun (x : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑(Fintype.card ι) : ℝ) * HPow.hPow (α := ℝ) 3 (Fintype.card ι - 1) * normBound b ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(Fintype.card ι) : ℝ) 1 + r)
Tactic: subst hd
Cleared hypotheses: d, hd, hr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
hr : r < -(↑(Fintype.card ι) : ℝ)
⊢ ∑ p ∈ Fintype.piFinset (δ := fun (x : ι) ↦ ℤ) fun (x : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑(Fintype.card ι) : ℝ) * HPow.hPow (α := ℝ) 3 (Fintype.card ι - 1) * normBound b ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(Fintype.card ι) : ℝ) 1 + r)
have set : let d := Fintype.card ι;
∀ (hr : r < -(↑d : ℝ)),
  ∑ p ∈ Fintype.piFinset (δ := fun (x : ι) ↦ ℤ) fun (x : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * normBound b ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: set d := Fintype.card ι
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
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_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
⊢ LE.le (α := ℝ) (-(↑d : ℝ)) 0
have linarith : LT.lt (α := ℝ) 0 (-(↑d : ℝ)) → HSub.hSub (α := ℝ) 0 (↑d : ℝ) + HSub.hSub (α := ℝ) 0 (-(↑d : ℝ)) = 0
Tactic: linarith