intro i j n hiP hix hij
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
⊢ ∀ (i j : ℕ) {n : ℕ}, i ∣ s.prodPrimes → i ∣ x → x ∣ j ^ n → i ∣ j
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
i j n : ℕ
hiP : i ∣ s.prodPrimes
hix : i ∣ x
hij : x ∣ j ^ n
⊢ i ∣ j