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
ι : 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 : ℝ)
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
hbc : 0 ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ LE.le (α := ℝ) (∑ k ∈ range n, HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
    (∑ k ∈ range (n + 1), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))

Tactic:
rw [Finset.sum_range_succ', le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right, Finset.sum_range_succ'
-- 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
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 : ℝ)
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + 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
ι : 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 : ℝ)
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
hbc :
  LE.le (α := ℝ) (∑ k ∈ range (n + 1), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
    (∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
⊢ HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑ k ∈ range (n + 1), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r) ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
gcongr
-- 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
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 : ℝ)
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
x : ℕ
h : x ∉ range (n + 1)
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑x : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + 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
ι : 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 : ℝ)
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
hbc : HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r < -1
⊢ LE.le (α := ℝ) (∑ k ∈ range (n + 1), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
    (∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))

Tactic:
refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)

Premises used: Iff.mpr, Summable.sum_le_tsum, Real.summable_nat_rpow
-- 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
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 : ℝ)
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
linarith : -1 ≤ HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r → r - -(↑d : ℝ) + (-1 - (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)) = 0
⊢ HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r < -1

Tactic:
linarith
-- 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
inl :
  Subsingleton.{u_1 + 1} ↥L →
    ∃ A > 0,
      ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
        ∀ (s : Finset ↥L),
          ∑ z ∈ s, ‖z‖ ^ r ≤
            A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)
inr :
  Nontrivial.{u_1} ↥L →
    ∃ A > 0,
      ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
        ∀ (s : Finset ↥L),
          ∑ z ∈ s, ‖z‖ ^ r ≤
            A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + 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
h : Subsingleton.{u_1 + 1} ↥L
⊢ ∃ A > 0,
    ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
⟨1, zero_lt_one, fun r hr s ↦ ?_⟩

Premises used: zero_lt_one, And.intro, Exists.intro, 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
h : Subsingleton.{u_1 + 1} ↥L
inl :
  ∀ (r : ℝ) (hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)) (s : Finset ↥L),
    ∑ z ∈ s, ‖z‖ ^ r ≤
      HPow.hPow (α := ℝ) 1 r *
        ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
refine ⟨1, zero_lt_one, fun r hr s ↦ ?_⟩
-- 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 : Subsingleton.{u_1 + 1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
s : Finset ↥L
linarith :
  r = 0 → HSub.hSub (α := ℝ) 0 (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) + (r - -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)) + -(r - 0) = 0
⊢ r ≠ 0

Tactic:
linarith
-- 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 : Subsingleton.{u_1 + 1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
s : Finset ↥L
⊢ r ≠ 0

Tactic:
have hr : r ≠ 0 := by linarith
-- 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 : Subsingleton.{u_1 + 1} ↥L
r : ℝ
hr_1 : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
s : Finset ↥L
hr : r ≠ 0
x : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑x : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + 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
h : Subsingleton.{u_1 + 1} ↥L
r : ℝ
hr_1 : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
s : Finset ↥L
hr : r ≠ 0
⊢ ∑ z ∈ s, ‖z‖ ^ r ≤
    HPow.hPow (α := ℝ) 1 r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
simpa [Subsingleton.elim _ (0 : L), Real.zero_rpow hr] using tsum_nonneg fun _ ↦ by positivity

Premises used: Real.zero_rpow, Subsingleton.elim, tsum_nonneg, 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
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
inr :
  ∀ (this : Fintype I),
    ∃ A > 0,
      ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
        ∀ (s : Finset ↥L),
          ∑ z ∈ s, ‖z‖ ^ r ≤
            A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
have : Fintype I := inferInstance
-- 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
inr :
  ∃ A > 0,
    ∀ r < -(↑(Fintype.card I) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(Fintype.card I) : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∀ r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) 1 + r)

Tactic:
simp_rw [Module.finrank_eq_card_basis b]

Premises used: Module.finrank_eq_card_basis
-- 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
inr :
  let d := Fintype.card I;
  ∃ A > 0,
    ∀ r < -(↑d : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∀ r < -(↑(Fintype.card I) : ℝ),
      ∀ (s : Finset ↥L),
        ∑ z ∈ s, ‖z‖ ^ r ≤
          A ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑(Fintype.card I) : ℝ) 1 + r)

Tactic:
set d := Fintype.card I

Premises used: Fintype.card
-- 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
⊢ d ≠ 0

Tactic:
simp [d]
-- 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
⊢ d ≠ 0

Tactic:
have hd : d ≠ 0 := by simp [d]
-- 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
⊢ HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) > 0

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
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
refine :
  ∀ (r : ℝ) (hr : r < -(↑d : ℝ)) (u : Finset ↥L),
    ∑ z ∈ u, ‖z‖ ^ r ≤
      HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
        ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ ∃ A > 0,
    ∃ B > 0,
      ∀ r < -(↑d : ℝ),
        ∀ (s : Finset ↥L),
          ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
refine ⟨2 * d * 3 ^ (d - 1), by positivity, ε, normBound_pos b, fun r hr u ↦ ?_⟩
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
u : Finset ↥L
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
⊢ (↑u : Set ↥L) =
    (↑(Finset.image (α := I → ℤ) (⇑e.toAddEquiv.toEmbedding : (a : I → ℤ) → ↥L)
          (Finset.image (⇑e.symm.toAddEquiv.toEmbedding : (a : ↥L) → I → ℤ) u)) :
      Set ↥L)

Tactic:
simpa using (e.image_symm_image _).symm

Premises used: LinearEquiv.toAddEquiv, Equiv.image_symm_image, AddEquiv.toEquiv, Eq.symm
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
u : Finset ↥L
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
obtain :
  ∀ (u : Finset (I → ℤ)),
    ∑ z ∈ Finset.image (⇑e.toAddEquiv.toEmbedding : (a : I → ℤ) → ↥L) u, ‖z‖ ^ r ≤
      HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
        ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ ∑ z ∈ u, ‖z‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
obtain ⟨u, rfl⟩ : ∃ u' : Finset _, u = u'.image e.toEmbedding :=
      ⟨u.image e.symm.toEmbedding, Finset.coe_injective
        (by simpa using (e.image_symm_image _).symm)⟩

Premises used: Finset, rfl
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
dsimp :
  ∑ z ∈ Finset.image (⇑e : (a : I → ℤ) → ↥L) u, ‖(↑z : E)‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ ∑ z ∈ Finset.image (⇑e.toAddEquiv.toEmbedding : (a : I → ℤ) → ↥L) u, ‖z‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
dsimp
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
simp :
  ∑ x ∈ u, norm.{u_1} (E := E) (↑((e : (a : I → ℤ) → ↥L) x) : E) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ ∑ z ∈ Finset.image (⇑e : (a : I → ℤ) → ↥L) u, ‖(↑z : E)‖ ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq, implies_true, Set.injOn_of_eq_iff_eq,
      Finset.sum_image, ge_iff_le]

Premises used: ge_iff_le, Set.injOn_of_eq_iff_eq, EmbeddingLike.apply_eq_iff_eq, Finset.sum_image, implies_true
-- 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
r : ℝ
hr : r < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
obtain :
  ∀ (r : ℝ) (hr : 0 < r) (hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r),
    ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)
⊢ ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)

Tactic:
obtain ⟨r, hr, hr'⟩ := u.finite_toSet.isCompact.isBounded.subset_closedBall_lt 0 0

Premises used: IsCompact.isBounded, Set.Finite.isCompact, Bornology.IsBounded.subset_closedBall_lt, Finset.finite_toSet, 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
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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
⊢ ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)

Tactic:
⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩

Premises used: Int.floor, Exists.intro, Int.toNat
-- 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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
refine :
  ∀ (x : I → ℤ) (hx : x ∈ u),
    Membership.mem (γ := Finset (I → ℤ))
      (Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑⌊r⌋.toNat : ℤ)) (↑⌊r⌋.toNat : ℤ)) x
⊢ ∃ (n : ℕ), u ⊆ Fintype.piFinset (δ := fun (a : I) ↦ ℤ) fun (x : I) ↦ Finset.Icc (-(↑n : ℤ)) (↑n : ℤ)

Tactic:
refine ⟨⌊r⌋.toNat, fun x hx ↦ ?_⟩
-- 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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
rw : 0 ≤ ⌊r⌋
⊢ max ⌊r⌋ 0 = ⌊r⌋

Tactic:
rw [sup_eq_left]

Premises used: sup_eq_left
-- 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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
⊢ 0 ≤ ⌊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
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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
⊢ max ⌊r⌋ 0 = ⌊r⌋

Tactic:
have hr'' : ⌊r⌋ ⊔ 0 = ⌊r⌋ := by rw [sup_eq_left]; 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
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
r_1 : ℝ
hr_1 : r_1 < -(↑d : ℝ)
e : (I → ℤ) ≃ₗ[ℤ] ↥L := LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℤ ℤ I)
u : Finset (I → ℤ)
r : ℝ
hr : 0 < r
hr' : (↑u : Set (I → ℤ)) ⊆ Metric.closedBall 0 r
x : I → ℤ
hx : x ∈ u
hr'' : max ⌊r⌋ 0 = ⌊r⌋
⊢ Membership.mem (γ := Set (I → ℤ)) (Metric.closedBall 0 r) x

Tactic:
have := hr' hx