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_1 : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
hk : k ∈ range n
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
this : HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 ≤ |v j|
⊢ LE.le (α := ℤ) ((↑(k + 1) : ℤ) : ℤ)
    (|((b.repr : (a : ↥L) → ι →₀ ℤ) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) : (a : ι) → ℤ)
          j| :
      ℤ)

Tactic:
simpa [Finsupp.single_apply] using this

Premises used: Finsupp.single_apply
-- 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 < ε
k : ℕ
hk : k ∈ range n
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
h : HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 ≤ |v j|
⊢ LE.le (α := ℤ) ((↑(k + 1) : ℤ) : ℤ)
    (|((b.repr : (a : ↥L) → ι →₀ ℤ) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) : (a : ι) → ℤ)
          j| :
      ℤ)

Tactic:
suffices ↑k + 1 ≤ |v j| by simpa [Finsupp.single_apply] using 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
ι : 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 < ε
k : ℕ
hk : k ∈ range n
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
h : ∀ (H : |v j| < HAdd.hAdd (α := ℤ) (↑k : ℤ) 1), False
⊢ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 ≤ |v j|

Tactic:
by_contra! H
-- 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 < ε
k : ℕ
hk : k ∈ range n
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
H : |v j| < HAdd.hAdd (α := ℤ) (↑k : ℤ) 1
⊢ Membership.mem (γ := Finset ℤ) (Icc (-(↑k : ℤ)) (↑k : ℤ)) (v j)

Tactic:
rw [Int.lt_add_one_iff, abs_le, ← Finset.mem_Icc] at H

Premises used: abs_le, Finset.mem_Icc, Int.lt_add_one_iff
-- 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 < ε
k : ℕ
hk : k ∈ range n
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
H : Membership.mem (γ := Finset ℤ) (Icc (-(↑k : ℤ)) (↑k : ℤ)) (v j)
⊢ False

Tactic:
hj H
-- 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 < ε
k : ℕ
hk : k ∈ range n
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
H : Membership.mem (γ := Finset ℤ) (Icc (-(↑k : ℤ)) (↑k : ℤ)) (v j)
⊢ False

Tactic:
exact hj H
-- 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 < ε
simp :
  LE.le (α := ℝ) (∑ x ∈ range n, (↑(#(s (x + 1) \ s x)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * ε) ^ r)
    (∑ k ∈ range n, (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)
⊢ LE.le (α := ℝ) (∑ k ∈ range n, ∑ p ∈ s (k + 1) \ s k, (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)
    (∑ k ∈ range n, (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)

Tactic:
simp only [sum_const, nsmul_eq_mul]

Premises used: nsmul_eq_mul, Finset.sum_const
-- 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 < ε
h : ∀ (k : ℕ) (hk : k ∈ range n), #(s (k + 1) \ s k) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)
⊢ LE.le (α := ℝ) (∑ x ∈ range n, (↑(#(s (x + 1) \ s x)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * ε) ^ r)
    (∑ k ∈ range n, (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)

Tactic:
gcongr with k hk
-- 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 < ε
k : ℕ
hk : k ∈ range n
⊢ #(s (k + 1) \ s k) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)

Tactic:
(this _).trans ?_

Premises used: 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
ι : 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 < ε
k : ℕ
hk : k ∈ range n
h : 2 * d * (2 * k + 3) ^ (d - 1) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)
⊢ #(s (k + 1) \ s k) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)

Tactic:
refine (this _).trans ?_

Premises used: 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
ι : 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 < ε
k : ℕ
hk : k ∈ range n
h : 2 * k + 3 ≤ 3 * (k + 1)
⊢ 2 * d * (2 * k + 3) ^ (d - 1) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)

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 < ε
k : ℕ
hk : k ∈ range n
⊢ 2 * k + 3 ≤ 3 * (k + 1)

Tactic:
lia
-- 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 < ε
simp_rw :
  Eq (α := ℝ) (∑ k ∈ range n, (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)
    (∑ i ∈ range n,
      HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
        (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ r))
⊢ ∑ k ∈ range n, (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑ k ∈ range n, HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r

Tactic:
simp_rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- 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 < ε
e_f :
  ∀ (k : ℕ),
    (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r =
      HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
        (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r)
⊢ Eq (α := ℝ) (∑ k ∈ range n, (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)
    (∑ i ∈ range n,
      HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
        (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ r))

Tactic:
congr with k
-- 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 < ε
k : ℕ
e_f :
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * (3 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ^ (d - 1) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r)
⊢ (↑(2 * d * (3 * (k + 1)) ^ (d - 1)) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r)

Tactic:
push_cast
-- 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 < ε
k : ℕ
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

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 < ε
k : ℕ
⊢ 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
ι : 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 < ε
k : ℕ
e_f :
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * (HPow.hPow (α := ℝ) 3 (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1)) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r * ε ^ r) =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r)
⊢ HMul.hMul (α := ℝ) 2 (↑d : ℝ) * (3 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ^ (d - 1) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r)

Tactic:
rw [Real.mul_rpow (by positivity) (by positivity), mul_pow]

Premises used: Real.mul_rpow, mul_pow
-- 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 < ε
k : ℕ
e_f e_f₁ e_f₂ e_f₃ :
  HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) (β := ℤ) 3 (↑(d - 1) : ℤ) *
          HPow.hPow (β := ℤ) (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) (↑(d - 1) : ℤ) *
        HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r *
      ε ^ r =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) (β := ℤ) 3 (↑(d - 1) : ℤ) * ε ^ r *
        HPow.hPow (β := ℤ) (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) (↑(d - 1) : ℤ) *
      HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r
⊢ HMul.hMul (α := ℝ) 2 (↑d : ℝ) * (HPow.hPow (α := ℝ) 3 (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1)) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r * ε ^ r) =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r)

Tactic:
group
-- 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 < ε
e_a :
  ∀ (k : ℕ),
    HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r =
      HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑ k ∈ range n, HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r =
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * ε ^ r *
      ∑ k ∈ range n, HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
congr with k
-- 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 < ε
k : ℕ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

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 < ε
k : ℕ
e_a :
  HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑d : ℝ) (↑1 : ℝ) + r) =
    HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r =
    HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
rw [← Real.rpow_natCast, ← Real.rpow_add (by positivity), Nat.cast_sub hd]

Premises used: Nat.cast_sub, Real.rpow_add, Real.rpow_natCast
-- 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 < ε
k : ℕ
e_a e_a₁ e_a₂ e_a₃ :
  HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) ((↑(d - 1) : ℝ) + r) = HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) ((↑(d - 1) : ℝ) + r)
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑d : ℝ) (↑1 : ℝ) + r) =
    HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)

Tactic:
norm_cast
-- 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, HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑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 ∈ range n, HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (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)

Tactic:
gcongr