-- 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 < ε
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)
calc₁ :
  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)
calc₂ :
  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)
calc₃ :
  ∑ 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
calc₄ :
  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)
calc₅ :
  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)
calc₆ :
  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)
⊢ ∑ 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:
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

Premises used: HSub.hSub, Nat.cast, Finset.range, HAdd.hAdd, OfNat.ofNat