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

case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∀ (i : ℕ), i ∈ Ioc k (max (k + 1) n) → ¬i ∈ Ioo k n → 0 ≤ (↑(i ^ 2))⁻¹
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∑ i in Ioo k n, (↑(i ^ 2))⁻¹ ≤ ∑ i in Ioc k (max (k + 1) n), (↑(i ^ 2))⁻¹
apply sum_le_sum_of_subset_of_nonneg
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ x ∈ Ioc k (max (k + 1) n)
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Ioo k n ⊆ Ioc k (max (k + 1) n)
intro x hx
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : k < x ∧ x < n
⊢ x ∈ Ioc k (max (k + 1) n)
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : x ∈ Ioo k n
⊢ x ∈ Ioc k (max (k + 1) n)
simp only [mem_Ioo] at hx
no goals
case h
α : Type u_1
inst✝ : LinearOrderedField α
k n x : ℕ
hx : k < x ∧ x < n
⊢ x ∈ Ioc k (max (k + 1) n)
simp only [hx, hx.2.le, mem_Ioc, le_max_iff, or_true_iff, and_self_iff]
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n i : ℕ
_hi : i ∈ Ioc k (max (k + 1) n)
_hident : ¬i ∈ Ioo k n
⊢ 0 ≤ (↑(i ^ 2))⁻¹
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∀ (i : ℕ), i ∈ Ioc k (max (k + 1) n) → ¬i ∈ Ioo k n → 0 ≤ (↑(i ^ 2))⁻¹
intro i _hi _hident
no goals
case hf
α : Type u_1
inst✝ : LinearOrderedField α
k n i : ℕ
_hi : i ∈ Ioc k (max (k + 1) n)
_hident : ¬i ∈ Ioo k n
⊢ 0 ≤ (↑(i ^ 2))⁻¹
positivity
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k ^ 2))⁻¹ + ∑ k in Ico (Nat.succ k + 1) (Nat.succ (max (k + 1) n)), (↑(k ^ 2))⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑(i ^ 2))⁻¹

case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k < Nat.succ (max (k + 1) n)
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ∑ i in Ioc k (max (k + 1) n), (↑(i ^ 2))⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑(i ^ 2))⁻¹
rw [← Nat.Icc_succ_left, ← Nat.Ico_succ_right, sum_eq_sum_Ico_succ_bot]
case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k < Nat.succ (max (k + 1) n)

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

case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k < Nat.succ (max (k + 1) n)
swap
no goals
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k ^ 2))⁻¹ + ∑ k in Ico (Nat.succ k + 1) (Nat.succ (max (k + 1) n)), (↑(k ^ 2))⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑(i ^ 2))⁻¹
rw [Nat.Ico_succ_right, Nat.Icc_succ_left, Nat.cast_pow, Nat.cast_succ]
no goals
case hab
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k < Nat.succ (max (k + 1) n)
exact Nat.succ_lt_succ ((Nat.lt_succ_self k).trans_le (le_max_left _ _))
case refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k ≠ 0

case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k))⁻¹ - (↑(max (Nat.succ k) n))⁻¹ ≤ (↑k + 1)⁻¹
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + ∑ i in Ioc (Nat.succ k) (max (k + 1) n), (↑(i ^ 2))⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹
refine' add_le_add le_rfl ((sum_Ioc_inv_sq_le_sub _ (le_max_left _ _)).trans _)
no goals
case refine'_1
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ Nat.succ k ≠ 0
simp only [Ne.def, Nat.succ_ne_zero, not_false_iff]
no goals
case refine'_2
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ (↑(Nat.succ k))⁻¹ - (↑(max (Nat.succ k) n))⁻¹ ≤ (↑k + 1)⁻¹
simp only [Nat.cast_succ, one_div, sub_le_self_iff, inv_nonneg, Nat.cast_nonneg]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
have A : (1 : α) ≤ k + 1 := by simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 + 1 / (↑k + 1) ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
simp_rw [← one_div]
case bc
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 ≤ 1 / (↑k + 1)
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 + 1 / (↑k + 1) ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
apply add_le_add_right
case bc
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ↑k + 1 ≤ (↑k + 1) ^ 2
case bc
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ 1 / (↑k + 1) ^ 2 ≤ 1 / (↑k + 1)
refine' div_le_div zero_le_one le_rfl (zero_lt_one.trans_le A) _
no goals
case bc
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
A : 1 ≤ ↑k + 1
⊢ ↑k + 1 ≤ (↑k + 1) ^ 2
simpa using pow_le_pow A one_le_two
no goals
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ 1 ≤ ↑k + 1
simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
no goals
α : Type u_1
inst✝ : LinearOrderedField α
k n : ℕ
⊢ 1 / (↑k + 1) + 1 / (↑k + 1) = 2 / (↑k + 1)
ring