Proving messy yet straightforward inequality

Stream: new members

[Isak Colboubrani]

What is the idiomatic approach to proving this seemingly messy yet straightforward inequality?

#mwe:

import Mathlib
open Nat
example (n : ℕ) : (2 * (6 + n))! / ((6 + n)! * (6 + n)!) ≤ 4 * ((2 * (5 + n))! / ((5 + n)! * (5 + n)!)) := by sorry

[Aaron Liu]

What's your reasoning for why this is true?

[Isak Colboubrani]

Sorry for the messy formatting, but this is my reasoning:

WTS: $\frac{(2(6+n))!}{((6+n)!)^2} \leq 4 \frac{(2(5+n))!}{((5+n)!)^2}$ (with $n \in \mathbb{N}$).

Let $k=n+5$.

Note that each algebraic manipulation below is reversible (multiplying by positive terms or canceling positive factors), so the first and last statements should be logically equivalent.

$\frac{(2(k+1))!}{((k+1)!)^2} \leq 4 \frac{(2(k))!}{((k)!)^2}$
$(2(k+1))! \cdot (k!)^2 \leq 4 (2k)! \cdot ((k+1)!)^2$
$(2(k+1))! \cdot (k!) \cdot (k!) \leq 4 (2k)! \cdot ((k+1)!) \cdot ((k+1)!)$
$(2(k+1))! \cdot (k!) \cdot (k!) \leq 4 (2k)! \cdot (k+1) \cdot (k+1) \cdot (k!) \cdot (k!)$
$(2(k+1))! \leq 4 (2k)! \cdot (k+1) \cdot (k+1)$
$(2k+2)! \leq 4 (2k)! \cdot (k+1) \cdot (k+1)$
$(2k + 2)(2k + 1)(2k)! \leq 4 (2k)! \cdot (k+1) \cdot (k+1)$
$(2k + 2)(2k + 1) \leq 4 \cdot (k+1) \cdot (k+1)$
$4k^2+6k+2 \leq 4k^2+8k+4$
$0 \leq 2k+2$ (and every step reversible)

[Aaron Liu]

Here's what I came up with:

import Mathlib
open Nat
example (n : ℕ) : (2 * (6 + n))! / ((6 + n)! * (6 + n)!) ≤ 4 * ((2 * (5 + n))! / ((5 + n)! * (5 + n)!)) := by
  simp_rw [← add_comm n, show 6 = 5 + 1 from rfl, ← add_assoc]
  generalize n + 5 = k
  clear n

  -- this part is converting to `ℚ` since division on `ℕ` is floor division and is less well-behaved than division on `ℚ`
  conv_lhs =>
    enter [2, 2, 1]
    equals 2 * (k + 1) - (k + 1) => rw [two_mul, add_tsub_cancel_right]
  conv_rhs =>
    enter [2, 2, 2, 1]
    equals 2 * k - k => rw [two_mul, add_tsub_cancel_right]
  have hk : k ≤ 2 * k := by
    rw [two_mul]
    exact Nat.le_add_right k k
  rw [← choose_eq_factorial_div_factorial (by simp), ← choose_eq_factorial_div_factorial hk]
  qify
  rw [cast_choose ℚ (by simp), cast_choose ℚ hk]
  simp_rw [two_mul, add_tsub_cancel_right]

  rw [← mul_div_assoc, div_le_div_iff₀ (by simp [factorial_ne_zero]) (by simp [factorial_ne_zero])]
  -- this part is unfolding the factorial
  simp_rw [← two_mul, mul_add, mul_one]
  conv in 2 * k + 2 =>
    equals 2 * k + 1 + 1 => rfl
  simp_rw [factorial_succ]
  push_cast

  have h := Nat.zero_le ((2 * k + 2) * (2 * k)! * (k)! * (k)!)
  qify at h
  linear_combination h