-- Mathlib/Data/Complex/Exponential.lean
theorem sum_div_factorial_le {α : Type*} [LinearOrderedField α] (n j : ℕ) (hn : 0 < n) :
    (∑ m ∈ range j with n ≤ m, (1 / m.factorial : α)) ≤ n.succ / (n.factorial * n) :=
  calc
    (∑ m ∈ range j with n ≤ m, (1 / m.factorial : α)) =
        ∑ m ∈ range (j - n), (1 / ((m + n).factorial : α))

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₄ : (n.succ - 1 : α) = n := by simp

Result:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Proof state:
case h.hba
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ ↑n.factorial * ↑n.succ ^ i✝ ≤ ↑(i✝ + n).factorial

Tactic:
rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]

Result:
case h.hba
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ n.factorial * n.succ ^ i✝ ≤ (n + i✝).factorial

Proof state:
case hab.a
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ x ∈ range (j - n), (↑(x + n).factorial)⁻¹ ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹

Tactic:
gcongr

Result:
case h.hba
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ ↑n.factorial * ↑n.succ ^ i✝ ≤ ↑(i✝ + n).factorial

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n) ≤ ↑n.succ / (↑n.factorial * ↑n)

Tactic:
gcongr

Result:
case hab
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n) ≤ ↑n.succ

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
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]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₃ : (n.factorial * n : α) ≠ 0 := by positivity

Result:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Proof state:
case h.hba
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
i✝ : ℕ
a✝ : i✝ ∈ range (j - n)
⊢ n.factorial * n.succ ^ i✝ ≤ (n + i✝).factorial

Tactic:
exact Nat.factorial_mul_pow_le_factorial

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
⊢ ↑n.factorial * ↑n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case hab
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n) ≤ ↑n.succ

Tactic:
apply sub_le_self

Result:
case hab.a
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ 0 ≤ ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
⊢ ↑n.succ - 1 = ↑n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹ = (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m

Tactic:
simp [mul_inv, ← mul_sum, ← sum_mul, mul_comm, inv_pow]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₂ : (n.succ : α) ≠ 0 := by positivity

Result:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ m ∈ range (j - n), 1 / ↑(m + n).factorial ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹

Tactic:
simp_rw [one_div]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ ∑ x ∈ range (j - n), (↑(x + n).factorial)⁻¹ ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₁ : (n.succ : α) ≠ 1 :=
  @Nat.cast_one α _ ▸ mt Nat.cast_inj.1 (mt Nat.succ.inj (pos_iff_ne_zero.1 hn))

Result:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
⊢ ↑n.succ ≠ 0

Tactic:
positivity

Result:
no goals