awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 * d * (2 * k + 3) ^ (d - 1) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)
have h : 2 * k + 3 ≤ 3 * (k + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 ∈ 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
have 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))
Tactic: simp_rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ 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))
have 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)
Tactic: congr with k
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 : ℕ
⊢ (↑(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)
have 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)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [Real.mul_rpow (by positivity) (by positivity), mul_pow]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 : ℕ
⊢ 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)
have 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
Tactic: group
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ 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)
have e_a : ∀ (k : ℕ),
  HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r =
    HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: congr with k
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (d - 1) * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ r =
    HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have e_a : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑d : ℝ) (↑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]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ^ (HSub.hSub (α := ℝ) (↑d : ℝ) (↑1 : ℝ) + r) =
    HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have e_a : HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) ((↑(d - 1) : ℝ) + r) = HPow.hPow (α := ℝ) (↑(k + 1) : ℝ) ((↑(d - 1) : ℝ) + r)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ 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)
have 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))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ 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))
have hbc : 0 ≤ HPow.hPow (α := ℝ) (↑0 : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
Tactic: rw [Finset.sum_range_succ', le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ 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)
have hbc : LE.le (α := ℝ) (∑ k ∈ range (n + 1), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
  (∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ LE.le (α := ℝ) (∑ k ∈ range (n + 1), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
    (∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r))
have hbc : HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r < -1
Tactic: refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r < -1
have linarith : -1 ≤ HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r → r - -(↑d : ℝ) + (-1 - (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
ι : Type u_3
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis.{u_3, 0, u_1} ι ℤ ↥L
n : ℕ
r : ℝ
s : (n : ℕ) → Finset ((a : ι) → ℤ) :=
  fun (n : ℕ) ↦ Fintype.piFinset (δ := fun (i : ι) ↦ ℤ) fun (i : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ)
d : ℕ := Fintype.card ι
hr : r < -(↑d : ℝ)
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 < ε
⊢ ∑ p ∈ Fintype.piFinset (δ := fun (x : ι) ↦ ℤ) fun (x : ι) ↦ Icc (-(↑n : ℤ)) (↑n : ℤ),
      norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    HMul.hMul (α := ℝ) 2 (↑d : ℝ) * HPow.hPow (α := ℝ) 3 (d - 1) * normBound b ^ r *
      ∑' (k : ℕ), HPow.hPow (α := ℝ) (↑k : ℝ) (HSub.hSub (α := ℝ) (↑d : ℝ) 1 + r)
have calc : Eq (α := ℝ) (∑ p ∈ s n, norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r)
  (∑ k ∈ range n,
    ∑ p ∈ s (k + 1) \ s k, norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (p i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r)
Tactic: calc ∑ p ∈ s n, ‖∑ i, p i • b i‖ ^ r
      = ∑ k ∈ range n, ∑ p ∈ (s (k + 1) \ s k), ‖∑ i, p i • b i‖ ^ r := by
        simp [Finset.sum_eq_sum_range_sdiff _ @hs, hs0, hr'.ne]
    _ ≤ ∑ k ∈ range n, ∑ p ∈ (s (k + 1) \ s k), ((k + 1) * ε) ^ r := by
        gcongr ∑ k ∈ Finset.range n, ∑ p ∈ (s (k + 1) \ s k), ?_ with k hk v hv
        rw [← Nat.cast_one, ← Nat.cast_add]
        refine Real.rpow_le_rpow_of_nonpos (by positivity) ?_ hr'.le
        obtain ⟨j, hj⟩ : ∃ i, v i ∉ Icc (-k : ℤ) k := by simpa [s] using (mem_sdiff.mp hv).2
        refine mul_comm _ ε ▸ le_norm_of_le_abs_repr b _ _ j ?_
        suffices ↑k + 1 ≤ |v j| by simpa [Finsupp.single_apply] using this
        by_contra! H
        rw [Int.lt_add_one_iff, abs_le, ← Finset.mem_Icc] at H
        exact hj H
    _ ≤ ∑ k ∈ range n, ↑(2 * d * (3 * (k + 1)) ^ (d - 1)) * ((k + 1) * ε) ^ r := by
        simp only [sum_const, nsmul_eq_mul]
        gcongr with k hk
        refine (this _).trans ?_
        gcongr
        lia
    _ = 2 * d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, (k + 1) ^ (d - 1) * (k + 1 : ℝ) ^ r := by
        simp_rw [Finset.mul_sum]
        congr with k
        push_cast
        rw [Real.mul_rpow (by positivity) (by positivity), mul_pow]
        group
    _ = 2 * d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range n, (↑(k + 1) : ℝ) ^ (d - 1 + r) := by
        congr with k
        rw [← Real.rpow_natCast, ← Real.rpow_add (by positivity), Nat.cast_sub hd]
        norm_cast
    _ ≤ 2 * d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), (k : ℝ) ^ (d - 1 + r) := by
        gcongr
        rw [Finset.sum_range_succ', le_add_iff_nonneg_right]
        positivity
    _ ≤ 2 * d * 3 ^ (d - 1) * ε ^ r * ∑' k : ℕ, (k : ℝ) ^ (d - 1 + r) := by
        gcongr
        refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)
        linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
⊢ ∃ 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)
have 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)
Tactic: cases subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
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)
⊢ ∃ 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)
have 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)
Tactic: cases subsingleton_or_nontrivial L
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
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)
have 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)
Tactic: refine ⟨1, zero_lt_one, fun r hr s ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Subsingleton.{u_1 + 1} ↥L
r : ℝ
hr : r < -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)
s : Finset ↥L
⊢ r ≠ 0
have linarith : r = 0 → HSub.hSub (α := ℝ) 0 (↑(finrank.{0, u_1} ℤ ↥L) : ℝ) + (r - -(↑(finrank.{0, u_1} ℤ ↥L) : ℝ)) + -(r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Subsingleton.{u_1 + 1} ↥L
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)
have hr₁ : r ≠ 0
Tactic: have hr : r ≠ 0 := by linarith
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥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)
have 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)
Tactic: have : Fintype I := inferInstance
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Summable (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
L : Submodule ℤ E
inst_3 : DiscreteTopology.{u_1} ↥L
h : Nontrivial.{u_1} ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥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)
have 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)
Tactic: simp_rw [Module.finrank_eq_card_basis b]