-- Mathlib/Analysis/PSeries.lean
theorem sum_Ioo_inv_sq_le (k n : ℕ) : (∑ i ∈ Ioo k n, (i ^ 2 : α)⁻¹) ≤ 2 / (k + 1) :=
  calc
    (∑ i ∈ Ioo k n, ((i : α) ^ 2)⁻¹) ≤ ∑ i ∈ Ioc k (max (k + 1) n), ((i : α) ^ 2)⁻¹

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ k.succ ≠ 0

Tactic:
simp only [Ne, Nat.succ_ne_zero, not_false_iff]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ x ∈ Ioc k ((k + 1) ⊔ n)

Tactic:
simp only [mem_Ioo] at hx

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : k < x ∧ x < n
⊢ x ∈ Ioc k ((k + 1) ⊔ n)

Proof state:
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n i : ℕ
_hi : i ∈ Ioc k ((k + 1) ⊔ n)
_hident : i ∉ Ioo k n
⊢ 0 ≤ (↑i ^ 2)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ 1 ≤ ↑k + 1

Tactic:
simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Ioo k n ⊆ Ioc k ((k + 1) ⊔ n)

Tactic:
intro x hx

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ x ∈ Ioc k ((k + 1) ⊔ n)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Tactic:
simp_rw [← one_div]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 + 1 / (↑k + 1) ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Tactic:
have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ ((k + 1) ⊔ n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹

Tactic:
refine add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub ?_ (le_max_left _ _)).trans ?_)

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ k.succ ≠ 0

case refine_2
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑k.succ)⁻¹ - (↑(k.succ ⊔ n))⁻¹ ≤ (↑k + 1)⁻¹

Proof state:
case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ k.succ < ((k + 1) ⊔ n).succ

Tactic:
exact Nat.succ_lt_succ ((Nat.lt_succ_self k).trans_le (le_max_left _ _))

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑k.succ)⁻¹ - (↑(k.succ ⊔ n))⁻¹ ≤ (↑k + 1)⁻¹

Tactic:
simp only [Nat.cast_succ, one_div, sub_le_self_iff, inv_nonneg, Nat.cast_nonneg]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : k < x ∧ x < n
⊢ x ∈ Ioc k ((k + 1) ⊔ n)

Tactic:
simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true, and_self_iff]

Result:
no goals

Proof state:
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∀ i ∈ Ioc k ((k + 1) ⊔ n), i ∉ Ioo k n → 0 ≤ (↑i ^ 2)⁻¹

Tactic:
intro i _hi _hident

Result:
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n i : ℕ
_hi : i ∈ Ioc k ((k + 1) ⊔ n)
_hident : i ∉ Ioo k n
⊢ 0 ≤ (↑i ^ 2)⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∑ i ∈ Ioc k ((k + 1) ⊔ n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ ((k + 1) ⊔ n), (↑i ^ 2)⁻¹

Tactic:
rw [← Nat.Icc_succ_left, ← Nat.Ico_succ_right, sum_eq_sum_Ico_succ_bot]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑k.succ ^ 2)⁻¹ + ∑ k ∈ Ico (k.succ + 1) ((k + 1) ⊔ n).succ, (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ ((k + 1) ⊔ n), (↑i ^ 2)⁻¹

case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ k.succ < ((k + 1) ⊔ n).succ

Proof state:
case bc.h
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ↑k + 1 ≤ (↑k + 1) ^ 2

Tactic:
simpa using pow_right_mono₀ A one_le_two

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑k.succ ^ 2)⁻¹ + ∑ k ∈ Ico (k.succ + 1) ((k + 1) ⊔ n).succ, (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ ((k + 1) ⊔ n), (↑i ^ 2)⁻¹

case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ k.succ < ((k + 1) ⊔ n).succ

Tactic:
swap

Result:
case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ k.succ < ((k + 1) ⊔ n).succ

α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑k.succ ^ 2)⁻¹ + ∑ k ∈ Ico (k.succ + 1) ((k + 1) ⊔ n).succ, (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ ((k + 1) ⊔ n), (↑i ^ 2)⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∑ i ∈ Ioo k n, (↑i ^ 2)⁻¹ ≤ ∑ i ∈ Ioc k ((k + 1) ⊔ n), (↑i ^ 2)⁻¹

Tactic:
apply sum_le_sum_of_subset_of_nonneg

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Ioo k n ⊆ Ioc k ((k + 1) ⊔ n)

case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∀ i ∈ Ioc k ((k + 1) ⊔ n), i ∉ Ioo k n → 0 ≤ (↑i ^ 2)⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ 1 / (↑k + 1) + 1 / (↑k + 1) = 2 / (↑k + 1)

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 + 1 / (↑k + 1) ≤ 1 / (↑k + 1) + 1 / (↑k + 1)

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ↑k + 1 ≤ (↑k + 1) ^ 2

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑k.succ ^ 2)⁻¹ + ∑ k ∈ Ico (k.succ + 1) ((k + 1) ⊔ n).succ, (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ ((k + 1) ⊔ n), (↑i ^ 2)⁻¹

Tactic:
rw [Nat.Ico_succ_right, Nat.Icc_succ_left, Nat.cast_succ]

Result:
no goals