[GOAL]
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#
[PROOFSTEP]
refine prod_congr ?_ fun _ _ ↦ rfl
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ filter Nat.Prime (range (n + 1 + 1)) = filter Nat.Prime (range (n + 1))
[PROOFSTEP]
rw [range_succ, filter_insert, if_neg fun h ↦ odd_iff_not_even.mp hn _]
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n
[PROOFSTEP]
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1
[GOAL]
m n : ℕ
⊢ (m + n)# = m# * ∏ p in filter Nat.Prime (Ico (m + 1) (m + n + 1)), p
[PROOFSTEP]
rw [primorial, primorial, ← Ico_zero_eq_range, ← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]
[GOAL]
case hab
m n : ℕ
⊢ 0 ≤ m + 1
case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1
m n : ℕ ⊢ Disjoint (filter Nat.Prime (Ico 0 (m + 1))) (filter Nat.Prime (Ico (m + 1) (m + n + 1)))
[PROOFSTEP]
exacts [Nat.zero_le _, add_le_add_right (Nat.le_add_right _ _) _,
  disjoint_filter_filter <| Ico_disjoint_Ico_consecutive _ _ _]
[GOAL]
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ filter Nat.Prime (Ico (m + 1) (m + n + 1))
⊢ p ∣ Nat.choose (m + n) m
[PROOFSTEP]
rw [mem_filter, mem_Ico] at hp 
[GOAL]
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ Nat.choose (m + n) m
[PROOFSTEP]
exact hp.2.dvd_choose_add hp.1.1 (h.trans_lt (m.lt_succ_self.trans_le hp.1.1)) (Nat.lt_succ_iff.1 hp.1.2)
[GOAL]
n : ℕ
⊢ n# ≤ 4 ^ n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n ihn
[GOAL]
case h
n : ℕ
ihn : ∀ (m : ℕ), m < n → m# ≤ 4 ^ m
⊢ n# ≤ 4 ^ n
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
ihn : ∀ (m : ℕ), m < zero → m# ≤ 4 ^ m
⊢ zero# ≤ 4 ^ zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
⊢ succ n# ≤ 4 ^ succ n
[PROOFSTEP]
rcases n.even_or_odd with (⟨m, rfl⟩ | ho)
[GOAL]
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)
[PROOFSTEP]
rcases m.eq_zero_or_pos with (rfl | hm)
[GOAL]
case h.succ.inl.intro.inl
ihn : ∀ (m : ℕ), m < succ (0 + 0) → m# ≤ 4 ^ m
⊢ succ (0 + 0)# ≤ 4 ^ succ (0 + 0)
[PROOFSTEP]
decide
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
m : ℕ
ihn : ∀ (m_1 : ℕ), m_1 < succ (m + m) → m_1# ≤ 4 ^ m_1
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
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
[PROOFSTEP]
rw [choose_symm_add, two_mul, add_right_comm]
[GOAL]
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)
[PROOFSTEP]
rw [← pow_add, add_right_comm]
[GOAL]
case h.succ.inr
n : ℕ
ihn : ∀ (m : ℕ), m < succ n → m# ≤ 4 ^ m
ho : Odd n
⊢ succ n# ≤ 4 ^ succ n
[PROOFSTEP]
rcases Decidable.eq_or_ne n 1 with (rfl | hn)
[GOAL]
case h.succ.inr.inl
ihn : ∀ (m : ℕ), m < succ 1 → m# ≤ 4 ^ m
ho : Odd 1
⊢ succ 1# ≤ 4 ^ succ 1
[PROOFSTEP]
decide
[GOAL]
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
[PROOFSTEP]
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
