α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ n ≤ m
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ n ≤ m
simp at hm
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ n ≤ m
tauto
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ m < j
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ m < j
simp at hm
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ m < j
tauto
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ n ≤ m
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ 1 / ↑(Nat.factorial m) = 1 / ↑(Nat.factorial ((fun m x => m - n) m hm + n))
rw [tsub_add_cancel_of_le]
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ n ≤ m
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m ∈ filter (fun k => n ≤ k) (range j)
⊢ n ≤ m
simp at *
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ n ≤ m
tauto
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
a₁ a₂ : ℕ
ha₁ : a₁ ∈ filter (fun k => n ≤ k) (range j)
ha₂ : a₂ ∈ filter (fun k => n ≤ k) (range j)
h : (fun m x => m - n) a₁ ha₁ = (fun m x => m - n) a₂ ha₂
⊢ a₁ = a₂
rwa [tsub_eq_iff_eq_add_of_le, tsub_add_eq_add_tsub, eq_comm, tsub_eq_iff_eq_add_of_le,
    add_left_inj, eq_comm] at h <;>
simp at * <;> aesop
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
b : ℕ
hb : b ∈ range (j - n)
⊢ b = b + n - n
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
b : ℕ
hb : b ∈ range (j - n)
⊢ b = (fun m x => m - n) (b + n) (_ : b + n ∈ filter (fun k => n ≤ k) (range j))
dsimp
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
b : ℕ
hb : b ∈ range (j - n)
⊢ b = b + n - n
rw [add_tsub_cancel_right]
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ x in range (j - n), (↑(Nat.factorial (x + n)))⁻¹ ≤ ∑ m in range (j - n), (↑(Nat.factorial n) * ↑(Nat.succ n) ^ m)⁻¹
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ m in range (j - n), 1 / ↑(Nat.factorial (m + n)) ≤ ∑ m in range (j - n), (↑(Nat.factorial n) * ↑(Nat.succ n) ^ m)⁻¹
simp_rw [one_div]
case h.h
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ ↑(Nat.factorial n) * ↑(Nat.succ n) ^ i✝ ≤ ↑(Nat.factorial (i✝ + n))
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ x in range (j - n), (↑(Nat.factorial (x + n)))⁻¹ ≤ ∑ m in range (j - n), (↑(Nat.factorial n) * ↑(Nat.succ n) ^ m)⁻¹
gcongr
case h.h
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ Nat.factorial n * Nat.succ n ^ i✝ ≤ Nat.factorial (n + i✝)
case h.h
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ ↑(Nat.factorial n) * ↑(Nat.succ n) ^ i✝ ≤ ↑(Nat.factorial (i✝ + n))
rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]
no goals
case h.h
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ Nat.factorial n * Nat.succ n ^ i✝ ≤ Nat.factorial (n + i✝)
exact Nat.factorial_mul_pow_le_factorial
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ m in range (j - n), (↑(Nat.factorial n) * ↑(Nat.succ n) ^ m)⁻¹ =
    (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m
simp [mul_inv, mul_sum.symm, sum_mul.symm, -Nat.factorial_succ, mul_comm, inv_pow]
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
have h₁ : (n.succ : α) ≠ 1 :=
  @Nat.cast_one α _ ▸ mt Nat.cast_inj.1 (mt Nat.succ.inj (pos_iff_ne_zero.1 hn))
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
have h₂ : (n.succ : α) ≠ 0 := by positivity
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
h₃ : ↑(Nat.factorial n) * ↑n ≠ 0
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
have h₃ : (n.factorial * n : α) ≠ 0 := by positivity
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
h₃ : ↑(Nat.factorial n) * ↑n ≠ 0
h₄ : ↑(Nat.succ n) - 1 = ↑n
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
h₃ : ↑(Nat.factorial n) * ↑n ≠ 0
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
have h₄ : (n.succ - 1 : α) = n := by simp
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
h₃ : ↑(Nat.factorial n) * ↑n ≠ 0
h₄ : ↑(Nat.succ n) - 1 = ↑n
⊢ (↑(Nat.factorial n))⁻¹ * ∑ m in range (j - n), (↑(Nat.succ n))⁻¹ ^ m =
    (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n)
rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
    ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
    mul_comm (n : α) n.factorial, mul_inv_cancel h₃, one_mul, mul_comm]
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
⊢ ↑(Nat.succ n) ≠ 0
positivity
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
⊢ ↑(Nat.factorial n) * ↑n ≠ 0
positivity
no goals
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑(Nat.succ n) ≠ 1
h₂ : ↑(Nat.succ n) ≠ 0
h₃ : ↑(Nat.factorial n) * ↑n ≠ 0
⊢ ↑(Nat.succ n) - 1 = ↑n
simp
case h
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n) ≤ ↑(Nat.succ n)
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ (↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)) / (↑(Nat.factorial n) * ↑n) ≤
    ↑(Nat.succ n) / (↑(Nat.factorial n) * ↑n)
gcongr
case h.a
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)
case h
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ↑(Nat.succ n) - ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n) ≤ ↑(Nat.succ n)
apply sub_le_self
no goals
case h.a
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ ↑(Nat.succ n) * (↑(Nat.succ n))⁻¹ ^ (j - n)
positivity