-- Mathlib/Analysis/PSeries.lean
theorem summable_schlomilch_iff {C : ℕ} {u : ℕ → ℕ} {f : ℕ → ℝ≥0}
    (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m)
    (h_pos : ∀ n, 0 < u n) (hu_strict : StrictMono u)
    (hC_nonzero : C ≠ 0) (h_succ_diff : SuccDiffBounded C u) :
    (Summable fun k : ℕ => (u (k + 1) - (u k : ℝ≥0)) * f (u k)) ↔ Summable f

Proof state:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ (Summable fun k => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f

Tactic:
simp only [← tsum_coe_ne_top_iff_summable, Ne, not_iff_not, ENNReal.coe_mul]

Result:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤ ↔ ∑' (b : ℕ), ↑(f b) = ⊤

Proof state:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
h_nonneg : ∀ (n : ℕ), 0 ≤ ↑(f n)
hC : ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k)) ≤ (↑(u 1) - ↑(u 0)) * ↑(f (u 0)) + ↑C * ∑' (k : ℕ), ↑(f k)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

Tactic:
simpa [add_eq_top, mul_ne_top, mul_eq_top, hC_nonzero] using eq_top_mono hC h

Result:
no goals

Proof state:
case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ⊤
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤

Tactic:
replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
  ENNReal.coe_le_coe.2 (hf hm hmn)

Result:
case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤

Proof state:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤ ↔ ∑' (b : ℕ), ↑(f b) = ⊤

Tactic:
constructor <;> intro h

Result:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ⊤
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤

Proof state:
case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
this : ∑ k ∈ range (u 0), ↑(f k) ≠ ⊤
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤

Tactic:
simpa [h, add_eq_top, this] using le_tsum_schlomilch hf h_pos hu_strict

Result:
no goals

Proof state:
case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤

Tactic:
have : ∑ k ∈ range (u 0), (f k : ℝ≥0∞) ≠ ∞ := sum_ne_top.2 fun a _ => coe_ne_top

Result:
case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
this : ∑ k ∈ range (u 0), ↑(f k) ≠ ⊤
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤

Proof state:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
h_nonneg : ∀ (n : ℕ), 0 ≤ ↑(f n)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

Tactic:
obtain hC := tsum_schlomilch_le hf h_pos h_nonneg hu_strict.monotone h_succ_diff

Result:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
h_nonneg : ∀ (n : ℕ), 0 ≤ ↑(f n)
hC : ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k)) ≤ (↑(u 1) - ↑(u 0)) * ↑(f (u 0)) + ↑C * ∑' (k : ℕ), ↑(f k)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

Proof state:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

Tactic:
replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
  ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)

Result:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

Proof state:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤

Tactic:
have h_nonneg : ∀ n, 0 ≤ (f n : ℝ≥0∞) := fun n =>
  ENNReal.coe_le_coe.2 (f n).2

Result:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
h_nonneg : ∀ (n : ℕ), 0 ≤ ↑(f n)
⊢ ∑' (b : ℕ), ↑(f b) = ⊤