simp_rw [Finset.mem_coe, Finset.mem_filter, Nat.mem_divisors] at *
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i : ℕ
hi : i ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
j : ℕ
hj : j ∈ ↑(Finset.filter (fun l => ↑l ^ 2 ≤ s.level) s.prodPrimes.divisors)
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
⊢ False
case calc_2
s : SelbergSieve
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
hnu : CompletelyMultiplicative s.nu
hnu_nonneg : ∀ (n : ℕ), 0 ≤ s.nu n
hnu_lt : ∀ (p : ℕ), p.Prime → p ∣ s.prodPrimes → s.nu p < 1
i j : ℕ
hij : i ≠ j
t : Finset ℕ
x : ℕ
hx : x ∈ t
hti : (x ∣ i ^ ⌊s.level⌋₊ ∧ i ^ ⌊s.level⌋₊ ≠ 0) ∧ i ∣ x
htj : (x ∣ j ^ ⌊s.level⌋₊ ∧ j ^ ⌊s.level⌋₊ ≠ 0) ∧ j ∣ x
hi : (i ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑i ^ 2 ≤ s.level
hj : (j ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0) ∧ ↑j ^ 2 ≤ s.level
⊢ False