awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
neg : A ≤ A ^ (-1 * r)
⊢ A ≤ A⁻¹ ^ r

Tactic:
rw [← Real.rpow_neg_one, ← Real.rpow_mul hA.le]

Premises used: Real.rpow_neg_one, LT.lt.le, Real.rpow_mul
-- 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ A ≤ A ^ (-1 * r)

Tactic:
Real.self_le_rpow_of_one_le (not_le.mp hA').le ?_

Premises used: not_le, LT.lt.le, Iff.mp, Real.self_le_rpow_of_one_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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
neg : 1 ≤ -1 * r
⊢ A ≤ A ^ (-1 * r)

Tactic:
refine Real.self_le_rpow_of_one_le (not_le.mp hA').le ?_

Premises used: not_le, LT.lt.le, Iff.mp, Real.self_le_rpow_of_one_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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
neg : r ≤ -1
⊢ 1 ≤ -1 * r

Tactic:
simp only [neg_mul, one_mul, le_neg (b := r)]

Premises used: le_neg, neg_mul, one_mul
-- 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ r ≤ -1

Tactic:
hr.le.trans ?_

Premises used: LT.lt.le, LE.le.trans
-- 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
neg : LE.le (α := ℝ) (-(↑d : ℝ)) (-1)
⊢ r ≤ -1

Tactic:
refine hr.le.trans ?_

Premises used: LT.lt.le, LE.le.trans
-- 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H :
  ∀ r < -(↑d : ℝ),
    ∀ (s : Finset ↥L),
      ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -(↑d : ℝ)
s : Finset ↥L
⊢ LE.le (α := ℝ) (-(↑d : ℝ)) (-1)

Tactic:
simpa [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- 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
⊢ 0 < tsumNormRPowBound L

Tactic:
(exists_finsetSum_norm_rpow_le_tsum L).choose_spec.1

Premises used: Exists.choose_spec, And.left, ZLattice.tsumNormRPowBound, ZLattice.exists_finsetSum_norm_rpow_le_tsum
-- 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
r : ℝ
h : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
s : Finset ↥L
⊢ ∑ z ∈ s, ‖z‖ ^ r ≤
    tsumNormRPowBound L ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
(exists_finsetSum_norm_rpow_le_tsum L).choose_spec.2 r h s

Premises used: Exists.choose_spec, And.right, ZLattice.tsumNormRPowBound, ZLattice.exists_finsetSum_norm_rpow_le_tsum
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : ↥L
⊢ 0 x ≤ ‖x‖ ^ r

Tactic:
positivity
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
⊢ ∑' (z : ↥L), ‖z‖ ^ r ≤
    tsumNormRPowBound L ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
Summable.tsum_le_of_sum_le (summable_norm_rpow L r hr) (tsumNormRPowBound_spec L r hr)

Premises used: ZLattice.tsumNormRPowBound_spec, ZLattice.summable_norm_rpow, Summable.tsum_le_of_sum_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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
inl : Subsingleton.{u_1 + 1} ↥L → Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
inr : Nontrivial.{u_1} ↥L → Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r

Tactic:
cases subsingleton_or_nontrivial L

Premises used: Membership.mem, Subtype, subsingleton_or_nontrivial
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Subsingleton.{u_1 + 1} ↥L
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r

Tactic:
.of_finite

Premises used: Summable.of_finite
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Subsingleton.{u_1 + 1} ↥L
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r

Tactic:
exact .of_finite
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r

Tactic:
Summable.of_norm_bounded_eventually
    (.mul_left ((1 / 2) ^ r) (summable_norm_rpow L r hr)) ?_

Premises used: HDiv.hDiv, ZLattice.summable_norm_rpow, Summable.mul_left, HPow.hPow, Summable.of_norm_bounded_eventually, OfNat.ofNat
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
inr : ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r
⊢ Summable (α := ℝ) fun (z : ↥L) ↦ ‖(↑z : E) - x‖ ^ r

Tactic:
refine Summable.of_norm_bounded_eventually
    (.mul_left ((1 / 2) ^ r) (summable_norm_rpow L r hr)) ?_

Premises used: HDiv.hDiv, ZLattice.summable_norm_rpow, Summable.mul_left, HPow.hPow, Summable.of_norm_bounded_eventually, OfNat.ofNat
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
⊢ IsClosed (↑L : Set E)

Tactic:
have H : IsClosed (X := E) L := @AddSubgroup.isClosed_of_discrete _ _ _ _ _
    L.toAddSubgroup (inferInstanceAs (DiscreteTopology L))
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
⊢ ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r

Tactic:
((Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
    (Metric.isBounded_closedBall (x := (0 : E)) (r := 2 * ‖x‖)) H).preimage_embedding
    (.subtype _)).subset ?_

Premises used: Metric.isBounded_closedBall, Set.Mem, Set.Finite.preimage_embedding, Filter.Eventually, setOf, DiscreteTopology.isDiscrete, Set.Finite, Set.Finite.subset, Metric.finite_isBounded_inter_isClosed, Function.Embedding.subtype
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
inr :
  Subset (α := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
⊢ ∀ᶠ (i : ↥L) in Filter.cofinite, ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r

Tactic:
refine ((Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete
    (Metric.isBounded_closedBall (x := (0 : E)) (r := 2 * ‖x‖)) H).preimage_embedding
    (.subtype _)).subset ?_

Premises used: Metric.isBounded_closedBall, Set.Finite.preimage_embedding, DiscreteTopology.isDiscrete, Set.Finite.subset, Metric.finite_isBounded_inter_isClosed, Function.Embedding.subtype
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
pos :
  ∀ (ht₁ : ‖t‖ = 0),
    Membership.mem (γ := Set ↥L)
      ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
        (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
      t
neg :
  ∀ (ht₁ : ¬‖t‖ = 0),
    Membership.mem (γ := Set ↥L)
      ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
        (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
      t
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t

Tactic:
by_cases ht₁ : ‖t‖ = 0
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ‖t‖ = 0
⊢ t = 0

Tactic:
simpa using ht₁
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ‖t‖ = 0
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t

Tactic:
simp [show t = 0 by simpa using ht₁]
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
pos :
  ∀ (ht₂ : ‖(↑t : E) - x‖ = 0),
    Membership.mem (γ := Set ↥L)
      ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
        (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
      t
neg :
  ∀ (ht₂ : ¬‖(↑t : E) - x‖ = 0),
    Membership.mem (γ := Set ↥L)
      ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
        (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
      t
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t

Tactic:
by_cases ht₂ : ‖t - x‖ = 0
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ‖(↑t : E) - x‖ = 0
⊢ (↑t : E) = x

Tactic:
simpa [sub_eq_zero] using ht₂

Premises used: sub_eq_zero
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ‖(↑t : E) - x‖ = 0
⊢ Membership.mem (γ := Set ↥L)
    ((⇑(Function.Embedding.subtype fun (x : E) ↦ x ∈ L) : (a : ↥L) → E) ⁻¹'
      (Metric.closedBall 0 (2 * ‖x‖) ∩ (↑L : Set E)))
    t

Tactic:
simpa [show t = x by simpa [sub_eq_zero] using ht₂, two_mul] using t.2

Premises used: two_mul, Subtype.property
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
⊢ 0 < finrank.{0, u_1} ℤ ↥L

Tactic:
have : 0 < Module.finrank ℤ L := Module.finrank_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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ 0 < 2⁻¹ * ‖t‖

Tactic:
positivity
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ 0 < ‖(↑t : E) - x‖

Tactic:
positivity
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ LT.lt (α := ℝ) (-(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)) 0

Tactic:
simpa
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
rw : (2⁻¹ * ‖t‖) ^ r < ‖(↑t : E) - x‖ ^ r
⊢ ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖

Tactic:
rw [← Real.rpow_lt_rpow_iff_of_neg (by positivity) (by positivity) (hr.trans (by simpa))]

Premises used: Real.rpow_lt_rpow_iff_of_neg, LT.lt.trans
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ 0 ≤ ‖(↑t : E) - x‖ ^ r

Tactic:
positivity
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ (2⁻¹ * ‖t‖) ^ r < ‖(↑t : E) - x‖ ^ r

Tactic:
simpa [Real.mul_rpow, abs_eq_self.mpr (show 0 ≤ ‖t - x‖ ^ r by positivity)] using ht

Premises used: Iff.mpr, Real.mul_rpow, abs_eq_self
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this : 0 < finrank.{0, u_1} ℤ ↥L
⊢ ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖

Tactic:
have : ‖t - x‖ < 2⁻¹ * ‖t‖ := by
    rw [← Real.rpow_lt_rpow_iff_of_neg (by positivity) (by positivity) (hr.trans (by simpa))]
    simpa [Real.mul_rpow, abs_eq_self.mpr (show 0 ≤ ‖t - x‖ ^ r by positivity)] using ht
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
⊢ ‖(↑t : E)‖ - ‖x‖ < 2⁻¹ * ‖t‖

Tactic:
have := (norm_sub_norm_le _ _).trans_lt this
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - ‖x‖ < 2⁻¹ * ‖t‖
⊢ ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖

Tactic:
rw [sub_lt_iff_lt_add, ← sub_lt_iff_lt_add', AddSubgroupClass.coe_norm] at this

Premises used: sub_lt_iff_lt_add', sub_lt_iff_lt_add, AddSubgroupClass.coe_norm
-- 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
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
x : E
h : Nontrivial.{u_1} ↥L
H : IsClosed (↑L : Set E)
t : ↥L
ht : Membership.mem (γ := Set ↥L) {x_1 : ↥L | (fun (i : ↥L) ↦ ‖‖(↑i : E) - x‖ ^ r‖ ≤ (1 / 2) ^ r * ‖i‖ ^ r) x_1}ᶜ t
ht₁ : ¬‖t‖ = 0
ht₂ : ¬‖(↑t : E) - x‖ = 0
this_1 : 0 < finrank.{0, u_1} ℤ ↥L
this_2 : ‖(↑t : E) - x‖ < 2⁻¹ * ‖t‖
this : ‖(↑t : E)‖ - 2⁻¹ * ‖(↑t : E)‖ < ‖x‖
linarith : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
linarith₁ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 2 * ‖x‖ < ‖(↑t : E)‖ → GT.gt (α := ℝ) 2 0
linarith₄ : 2 * ‖x‖ < ‖(↑t : E)‖ → 2 / 2 = 1
linarith₅ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₆ : 2 * ‖x‖ < ‖(↑t : E)‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₇ : 2 * ‖x‖ < ‖(↑t : E)‖ → GT.gt (α := ℝ) 2 0
linarith₈ :
  2 * ‖x‖ < ‖(↑t : E)‖ →
    2 * ‖(↑t : E)‖ - HMul.hMul (α := ℝ) 1 1 * (1 * ‖(↑t : E)‖) - 2 * ‖x‖ + (2 * ‖x‖ - ‖(↑t : E)‖) = 0
⊢ ‖(↑t : E)‖ ≤ 2 * ‖x‖

Tactic:
linarith