-- Mathlib/Analysis/PSeries.lean
theorem summable_schlomilch_iff_of_nonneg {C : ℕ} {u : ℕ → ℕ} {f : ℕ → ℝ} (h_nonneg : ∀ n, 0 ≤ f n)
    (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

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

Tactic:
have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le

Result:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
k : ℕ
this : ↑(u k) ≤ ↑(u k.succ)
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(↑(u (k + 1)) - ↑(u k))

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

Tactic:
simp_rw [this]

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

Proof state:
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
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:
lift f to ℕ → ℝ≥0 using h_nonneg

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

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

Tactic:
exact_mod_cast NNReal.summable_schlomilch_iff hf h_pos hu_strict hC_nonzero h_succ_diff

Result:
no goals

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

Tactic:
have (k : ℕ) : (u (k + 1) - (u k : ℝ)) = ((u (k + 1) : ℝ≥0) - (u k : ℝ≥0) : ℝ≥0) := by
  have := Nat.cast_le (α := ℝ≥0).mpr <| (hu_strict k.lt_succ_self).le
  simp [NNReal.coe_sub this]

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

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

Tactic:
simp only [NNReal.coe_le_coe] at *

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

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

Tactic:
simp [NNReal.coe_sub this]

Result:
no goals