case h
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
induction' n using Nat.strong_induction_on with n IH
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n

case h.inr.inl
n : ℕ
n_big✝ : 4 ≤ n
IH : ∀ (m : ℕ), m < 4 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

case h.inr.inr
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * centralBinom n
case h
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
rcases lt_trichotomy n 4 with (hn | rfl | hn)
case h.inr.inr.intro
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * centralBinom (n + 1)
case h.inr.inr
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * centralBinom n
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.not_eq_zero_of_lt hn)
no goals
case h.inr.inr.intro
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * centralBinom (n + 1)
calc
  4 ^ (n + 1) < 4 * (n * centralBinom n) := lt_of_eq_of_lt (pow_succ'' n 4) $
    (mul_lt_mul_left <| zero_lt_four' ℕ).mpr (IH n n.lt_succ_self (Nat.le_of_lt_succ hn))
  _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
  _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
clear IH
no goals
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
exact False.elim ((not_lt.2 n_big) hn)
no goals
case h.inr.inl
n : ℕ
n_big✝ : 4 ≤ n
IH : ∀ (m : ℕ), m < 4 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4
norm_num [centralBinom, choose]
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * centralBinom n ≤ 2 * (2 * n + 1) * centralBinom n
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * centralBinom n) ≤ 2 * (2 * n + 1) * centralBinom n
rw [← mul_assoc]
no goals
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * centralBinom n ≤ 2 * (2 * n + 1) * centralBinom n
linarith