case h
n : ℕ
ihn : ∀ (m : ℕ), m < n → m# ≤ 4 ^ m
⊢ n# ≤ 4 ^ n
n : ℕ
⊢ n# ≤ 4 ^ n
induction' n using Nat.strong_induction_on with n ihn
case h.zero
ihn : ∀ (m : ℕ), m < zero → m# ≤ 4 ^ m
⊢ zero# ≤ 4 ^ zero

case h.succ
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
⊢ succ n# ≤ 4 ^ succ n
case h
n : ℕ
ihn : ∀ (m : ℕ), m < n → m# ≤ 4 ^ m
⊢ n# ≤ 4 ^ n
cases' n with n
case h.succ.inl.intro
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
⊢ succ (m + m)# ≤ 4 ^ succ (m + m)

case h.succ.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
⊢ succ n# ≤ 4 ^ succ n
case h.succ
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
⊢ succ n# ≤ 4 ^ succ n
rcases n.even_or_odd with (⟨m, rfl⟩ | ho)
no goals
case h.zero
ihn : ∀ (m : ℕ), m < zero → m# ≤ 4 ^ m
⊢ zero# ≤ 4 ^ zero
rfl
case h.succ.inl.intro.inl
ihn : ∀ (m : ℕ), m < succ (0 + 0) → m# ≤ 4 ^ m
⊢ succ (0 + 0)# ≤ 4 ^ succ (0 + 0)

case h.succ.inl.intro.inr
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ succ (m + m)# ≤ 4 ^ succ (m + m)
case h.succ.inl.intro
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
⊢ succ (m + m)# ≤ 4 ^ succ (m + m)
rcases m.eq_zero_or_pos with (rfl | hm)
no goals
case h.succ.inl.intro.inr
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ succ (m + m)# ≤ 4 ^ succ (m + m)
calc
  (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
  _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
  _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
  _ ≤ 4 ^ (m + 1) * 4 ^ m :=
    mul_le_mul' (ihn _ <| succ_lt_succ <| (lt_add_iff_pos_left _).2 hm) (choose_middle_le_pow _)
  _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
no goals
case h.succ.inl.intro.inl
ihn : ∀ (m : ℕ), m < succ (0 + 0) → m# ≤ 4 ^ m
⊢ succ (0 + 0)# ≤ 4 ^ succ (0 + 0)
decide
no goals
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#
rw [add_right_comm]
no goals
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + 1)# * Nat.choose (m + 1 + m) (m + 1) = (m + 1)# * Nat.choose (2 * m + 1) m
rw [choose_symm_add, two_mul, add_right_comm]
no goals
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ 4 ^ (m + 1) * 4 ^ m ≤ 4 ^ (m + m + 1)
rw [← pow_add, add_right_comm]
case h.succ.inr.inl
ihn : ∀ (m : ℕ), m < succ 1 → m# ≤ 4 ^ m
ho : Odd 1
⊢ succ 1# ≤ 4 ^ succ 1

case h.succ.inr.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
hn : n ≠ 1
⊢ succ n# ≤ 4 ^ succ n
case h.succ.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
⊢ succ n# ≤ 4 ^ succ n
rcases Decidable.eq_or_ne n 1 with (rfl | hn)
no goals
case h.succ.inr.inl
ihn : ∀ (m : ℕ), m < succ 1 → m# ≤ 4 ^ m
ho : Odd 1
⊢ succ 1# ≤ 4 ^ succ 1
decide
no goals
case h.succ.inr.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
hn : n ≠ 1
⊢ succ n# ≤ 4 ^ succ n
calc
  (n + 1)# = n# := primorial_succ hn ho
  _ ≤ 4 ^ n := ihn n n.lt_succ_self
  _ ≤ 4 ^ (n + 1) := pow_le_pow_of_le_right four_pos n.le_succ