rw [← Finset.filter_union]
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a) ∪ Finset.Ico (Nat.succ a) (Nat.succ b)), x