n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ filter Nat.Prime (range (n + 1 + 1)) = filter Nat.Prime (range (n + 1))
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#
refine prod_congr ?_ fun _ _ ↦ rfl
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ filter Nat.Prime (range (n + 1 + 1)) = filter Nat.Prime (range (n + 1))
rw [range_succ, filter_insert, if_neg fun h ↦ odd_iff_not_even.mp hn _]
no goals
n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ Nat.Prime (n + 1) → Even n
exact fun h ↦ h.even_sub_one <| mt succ.inj hn1