awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
obtain ⟨ε, hε, hε'⟩ := Metric.isOpen_iff.mp this 0 (by simp)

Premises used: Metric.isOpen_iff, Iff.mp, OfNat.ofNat
-- 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))
ε : ℝ
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 < ε / 2

Tactic:
positivity
-- 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))
ε : ℝ
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))
refine : ∀ (x : ↥L) (i : ι), ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
refine ⟨ε / 2, by positivity, fun x 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
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‖
neg : ∀ (hx : ¬x = 0), ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
by_cases hx : x = 0
-- 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))
ε : ℝ
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‖

Tactic:
simp [hx]
-- 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))
ε : ℝ
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
⊢ ‖(↑x : E)‖ ≠ 0

Tactic:
simpa
-- 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))
ε : ℝ
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
⊢ ‖(↑x : E)‖ ≠ 0

Tactic:
have hx : ‖x.1‖ ≠ 0 := by simpa
-- 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))
ε : ℝ
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
⊢ Membership.mem (γ := Set E) (Metric.ball 0 ε) ((ε / 2) • ‖x‖⁻¹ • (↑x : E))

Tactic:
simpa [norm_smul, inv_mul_cancel₀ hx, abs_eq_self.mpr hε.le]

Premises used: Iff.mpr, norm_smul, LT.lt.le, abs_eq_self, inv_mul_cancel₀
-- 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))
ε : ℝ
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 * (‖x‖⁻¹ * (↑((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i) : ℝ))| < 1

Tactic:
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

Premises used: trivial, abs_lt
-- 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))
ε : ℝ
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 * (‖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
-- 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_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 : ‖x‖⁻¹ * (|ε / 2| * |(↑((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i) : ℝ)|) < 1
⊢ 0 < ‖x‖

Tactic:
positivity
-- 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_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| * |(↑((((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i) : ℝ)| < ‖x‖
⊢ 0 ≤ ε / 2

Tactic:
positivity
-- 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_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‖

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

Premises used: Iff.mpr, Int.cast_abs, abs_inv, inv_mul_lt_iff₀, abs_mul, mul_left_comm, abs_norm, mul_one, abs_eq_self
-- 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_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 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) < ‖x‖
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
this.le

Premises used: LT.lt.le
-- 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_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 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) < ‖x‖
⊢ ε / 2 * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
exact this.le

Premises used: LT.lt.le
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
⊢ 0 < normBound b

Tactic:
(exists_forall_abs_repr_le_norm b).choose_spec.1

Premises used: Exists.choose_spec, ZLattice.exists_forall_abs_repr_le_norm, And.left, ZLattice.normBound
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
i : ι
⊢ normBound b * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
(exists_forall_abs_repr_le_norm b).choose_spec.2 x i

Premises used: Exists.choose_spec, ZLattice.exists_forall_abs_repr_le_norm, And.right, ZLattice.normBound
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
i : ι
rw : normBound b * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖
⊢ (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ (normBound b)⁻¹ * ‖x‖

Tactic:
rw [le_inv_mul_iff₀ (normBound_pos b)]

Premises used: le_inv_mul_iff₀, ZLattice.normBound_pos
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
i : ι
⊢ normBound b * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
normBound_spec b x i

Premises used: ZLattice.normBound_spec
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
i : ι
⊢ normBound b * (↑|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℝ) ≤ ‖x‖

Tactic:
exact normBound_spec b x i

Premises used: ZLattice.normBound_spec
-- 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_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 : ℤ) : ℤ)

Tactic:
Int.cast_lt.mp ((abs_repr_le b x i).trans_lt ?_)

Premises used: Int.cast_lt, Iff.mp, LE.le.trans_lt, ZLattice.abs_repr_le
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
hxn : ‖x‖ < normBound b * (↑n : ℝ)
i : ι
refine : (normBound b)⁻¹ * ‖x‖ < (↑(↑n : ℤ) : ℝ)
⊢ LT.lt (α := ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ) ((↑n : ℤ) : ℤ)

Tactic:
refine Int.cast_lt.mp ((abs_repr_le b x i).trans_lt ?_)

Premises used: Int.cast_lt, Iff.mp, LE.le.trans_lt, ZLattice.abs_repr_le
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
hxn : ‖x‖ < normBound b * (↑n : ℝ)
i : ι
rwa rwa₁ rwa₂ rwa₃ : ‖x‖ < normBound b * (↑(↑n : ℤ) : ℝ)
⊢ (normBound b)⁻¹ * ‖x‖ < (↑(↑n : ℤ) : ℝ)

Tactic:
rwa [inv_mul_lt_iff₀ (normBound_pos b)]

Premises used: inv_mul_lt_iff₀, ZLattice.normBound_pos
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
i : ι
hi : LE.le (α := ℤ) ((↑n : ℤ) : ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ)
contrapose! :
  ∀ (hi : ‖x‖ < normBound b * (↑n : ℝ)),
    LT.lt (α := ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ) ((↑n : ℤ) : ℤ)
⊢ normBound b * (↑n : ℝ) ≤ ‖x‖

Tactic:
contrapose! hi
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
i : ι
hi : ‖x‖ < normBound b * (↑n : ℝ)
⊢ LT.lt (α := ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ) ((↑n : ℤ) : ℤ)

Tactic:
abs_repr_lt_of_norm_lt b x n hi i

Premises used: ZLattice.abs_repr_lt_of_norm_lt
-- 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_3
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
x : ↥L
n : ℕ
i : ι
hi : ‖x‖ < normBound b * (↑n : ℝ)
⊢ LT.lt (α := ℤ) (|(((b.repr : (a : ↥L) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) i| : ℤ) ((↑n : ℤ) : ℤ)

Tactic:
exact abs_repr_lt_of_norm_lt b x n hi i

Premises used: ZLattice.abs_repr_lt_of_norm_lt