-- Mathlib/Analysis/SpecialFunctions/Stirling.lean
theorem log_stirlingSeq_sub_log_stirlingSeq_succ (n : ℕ) :
    log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤ 1 / (4 * (↑(n + 1) : ℝ) ^ 2)

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 / (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) ≤ 1 / (4 * (↑n + 1) ^ 2)

Tactic:
rw [div_le_div_iff₀ h₂ h₁]

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 * (4 * (↑n + 1) ^ 2) ≤ 1 * (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2)

Proof state:
n : ℕ
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Tactic:
have h₁ : (0 : ℝ) < 4 * ((n : ℝ) + 1) ^ 2 := by positivity

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 * (4 * (↑n + 1) ^ 2) ≤ 1 * (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2)

Tactic:
field_simp [h₃.ne']

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 / (2 * (↑n + 1) + 1) ^ 2 ≤ ((2 * (↑n + 1) + 1) ^ 2 - 1) / (2 * (↑n + 1) + 1) ^ 2

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2

Tactic:
rw [← mul_lt_mul_right h₃]

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Tactic:
refine (log_stirlingSeq_diff_le_geo_sum n).trans ?_

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + n * 8 + n ^ 2 * 4 ≤ 8 + n * 12 + n ^ 2 * 4

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ 0 < (2 * (↑n + 1) + 1) ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + ↑n * 8 + ↑n ^ 2 * 4 ≤ 8 + ↑n * 12 + ↑n ^ 2 * 4

Tactic:
norm_cast

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + n * 8 + n ^ 2 * 4 ≤ 8 + n * 12 + n ^ 2 * 4

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Tactic:
have h₂ : (0 : ℝ) < 1 - (1 / (2 * ((n : ℝ) + 1) + 1)) ^ 2 := by
  rw [← mul_lt_mul_right h₃]
  have H : 0 < (2 * ((n : ℝ) + 1) + 1) ^ 2 - 1 := by nlinarith [@cast_nonneg ℝ _ n]
  convert H using 1 <;> field_simp [h₃.ne']

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2

Tactic:
have H : 0 < (2 * ((n : ℝ) + 1) + 1) ^ 2 - 1 := by nlinarith [@cast_nonneg ℝ _ n]

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2

Proof state:
n : ℕ
⊢ 0 < 4 * (↑n + 1) ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Tactic:
push_cast

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 / (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) ≤ 1 / (4 * (↑n + 1) ^ 2)

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Tactic:
have h₃ : (0 : ℝ) < (2 * ((n : ℝ) + 1) + 1) ^ 2 := by positivity

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ Real.log (stirlingSeq (n + 1)) - Real.log (stirlingSeq (n + 2)) ≤ 1 / (4 * ↑(n + 1) ^ 2)

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 / (2 * (↑n + 1) + 1) ^ 2 ≤ ((2 * (↑n + 1) + 1) ^ 2 - 1) / (2 * (↑n + 1) + 1) ^ 2

Tactic:
rw [div_le_div_iff_of_pos_right h₃]

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 ≤ (2 * (↑n + 1) + 1) ^ 2 - 1

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
⊢ 0 < (2 * (↑n + 1) + 1) ^ 2 - 1

Tactic:
nlinarith [@cast_nonneg ℝ _ n]

Result:
no goals

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
H : 0 < (2 * (↑n + 1) + 1) ^ 2 - 1
⊢ 0 * (2 * (↑n + 1) + 1) ^ 2 < (1 - (1 / (2 * (↑n + 1) + 1)) ^ 2) * (2 * (↑n + 1) + 1) ^ 2

Tactic:
convert H using 1 <;> field_simp [h₃.ne']

Result:
no goals

Proof state:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 * (↑n + 1) ^ 2 ≤ (2 * (↑n + 1) + 1) ^ 2 - 1

Tactic:
ring_nf

Result:
n : ℕ
h₁ : 0 < 4 * (↑n + 1) ^ 2
h₃ : 0 < (2 * (↑n + 1) + 1) ^ 2
h₂ : 0 < 1 - (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ 4 + ↑n * 8 + ↑n ^ 2 * 4 ≤ 8 + ↑n * 12 + ↑n ^ 2 * 4