awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : 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 : ℝ)
⊢ ∑ 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 hr' : r < 0
Tactic: have hr' : r < 0 := hr.trans_le (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
ι : 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
⊢ ∑ 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 pos : ∀ (hd : d = 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)
Tactic: by_cases hd : d = 0
-- 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
pos :
  ∀ (hd : d = 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)
⊢ ∑ 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 neg : ∀ (hd : ¬d = 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)
Tactic: by_cases hd : d = 0
-- 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
ι : 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 : d = 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 this : IsEmpty ι
Tactic: have : IsEmpty ι := Fintype.card_eq_zero_iff.mp 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 : ¬d = 0
⊢ 1 ≤ d
have rwa : d ≠ 0
Tactic: rwa [Nat.one_le_iff_ne_zero]
-- 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
ι : 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 : ¬d = 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 hd₁ : 1 ≤ d
Tactic: replace hd : 1 ≤ d := by rwa [Nat.one_le_iff_ne_zero]
Cleared hypotheses: 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
⊢ s 0 = {0}
have h : ∀ (a : (a : ι) → ℤ), a ∈ s 0 ↔ Membership.mem (γ := Finset ((a : ι) → ℤ)) {0} a
Tactic: ext
-- 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
ι : 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
⊢ ∑ 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 hs0 : s 0 = {0}
Tactic: have hs0 : s 0 = {0} := by ext; simp [s, funext_iff]
-- 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
ι : 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}
⊢ ∑ 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 hs : ∀ {a b : ℕ} (ha : a ≤ b), s a ⊆ s b
Tactic: have hs {a b : ℕ} (ha : a ≤ b) : s a ⊆ s b := by grind
-- 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
k : ℕ
⊢ #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
have simp : (HAdd.hAdd (α := ℤ) (↑(k + 1) : ℤ) 1 - -(↑(k + 1) : ℤ)).toNat ^ card.{u_3} (α := ι) univ -
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - -(↑k : ℤ)).toNat ^ card.{u_3} (α := ι) univ ≤
  2 * d * (2 * k + 3) ^ (d - 1)
Tactic: simp only [le_add_iff_nonneg_right, zero_le, hs, card_sdiff_of_subset, s, Fintype.card_piFinset,
      Int.card_Icc, prod_const]
-- 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
ι : 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
⊢ ∑ 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 this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
Tactic: have (k : ℕ) : #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1) := by
    simp only [le_add_iff_nonneg_right, zero_le, hs, card_sdiff_of_subset, s, Fintype.card_piFinset,
      Int.card_Icc, prod_const]
    grind [abs_pow_sub_pow_le (α := ℤ) (2 * k + 3) (2 * k + 1) d]
-- 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
ι : 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
⊢ ∑ 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 hε : 0 < ε
Tactic: have hε : 0 < ε := normBound_pos b
-- 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,
      ∑ p ∈ s (k + 1) \ s k,
        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, (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r)
have h : ∀ (k : ℕ) (hk : k ∈ range n) (v : (a : ι) → ℤ) (hv : v ∈ s (k + 1) \ s k),
  norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r
Tactic: gcongr ∑ k ∈ Finset.range n, ∑ p ∈ (s (k + 1) \ s k), ?_ with k hk v hv
-- 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
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
⊢ norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * ε) ^ r
have h : norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤ ((↑(k + 1) : ℝ) * ε) ^ r
Tactic: rw [← Nat.cast_one, ← Nat.cast_add]
-- 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
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
⊢ norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) ^ r ≤ ((↑(k + 1) : ℝ) * ε) ^ r
have h : (↑(k + 1) : ℝ) * ε ≤ norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L))
Tactic: refine Real.rpow_le_rpow_of_nonpos (by positivity) ?_ hr'.le
-- 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
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
⊢ (↑(k + 1) : ℝ) * ε ≤ norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L))
have h : ∀ (j : ι) (hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)),
  (↑(k + 1) : ℝ) * ε ≤ norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L))
Tactic: obtain ⟨j, hj⟩ : ∃ i, v i ∉ Icc (-k : ℤ) k := by simpa [s] using (mem_sdiff.mp hv).2
-- 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
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
⊢ (↑(k + 1) : ℝ) * ε ≤ norm.{u_1} (E := ↥L) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L))
have h : LE.le (α := ℤ) ((↑(k + 1) : ℤ) : ℤ)
  (|((b.repr : (a : ↥L) → ι →₀ ℤ) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) : (a : ι) → ℤ) j| :
    ℤ)
Tactic: refine mul_comm _ ε ▸ le_norm_of_le_abs_repr b _ _ j ?_
-- 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
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
⊢ LE.le (α := ℤ) ((↑(k + 1) : ℤ) : ℤ)
    (|((b.repr : (a : ↥L) → ι →₀ ℤ) (∑ i : ι, HSMul.hSMul (β := ↥L) (v i) ((b : (a : ι) → ↥L) i : ↥L)) : (a : ι) → ℤ)
          j| :
      ℤ)
have h : HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 ≤ |v j|
Tactic: suffices ↑k + 1 ≤ |v j| by simpa [Finsupp.single_apply] using this
-- 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
v : (a : ι) → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-(↑k : ℤ)) (↑k : ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 ≤ |v j|
have h : ∀ (H : |v j| < HAdd.hAdd (α := ℤ) (↑k : ℤ) 1), False
Tactic: by_contra! H
-- 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
ι : 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
⊢ False
have H₁ : Membership.mem (γ := Finset ℤ) (Icc (-(↑k : ℤ)) (↑k : ℤ)) (v j)
Tactic: rw [Int.lt_add_one_iff, abs_le, ← Finset.mem_Icc] at H
Cleared hypotheses: H
-- 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, ∑ 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)
have 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)
Tactic: simp only [sum_const, nsmul_eq_mul]
-- 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 (α := ℝ) (∑ 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)
have h : ∀ (k : ℕ) (hk : k ∈ range n), #(s (k + 1) \ s k) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)
Tactic: gcongr with k hk
-- 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
⊢ #(s (k + 1) \ s k) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)
have h : 2 * d * (2 * k + 3) ^ (d - 1) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)
Tactic: refine (this _).trans ?_