specialize hti hx
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 ℕ
hti : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
⊢ 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 : ℕ
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 ℕ
htj : t ≤ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) j
x : ℕ
hx : x ∈ t
hti : x ∈ (fun l => Finset.filter (fun x => l ∣ x) (l ^ ⌊s.level⌋₊).divisors) i
⊢ False