Covering \N with powers of non-perfect powers

Stream: lean4

[max]

Sorry for the spam. I'm new to lean and trying to work through an analysis textbook.
One of the exercises (Understanding Analysis 2nd Ed 1.2.4) is to find an infinite set of infinite Sets that are all pairwise disjoint, but the union of all is equal to N.

My solution was to take the non-perfect powers https://oeis.org/A007916 and just take their powers as the sets Ai, and just tack on 0 and 1 to A1.

Alternatively, I could just prove that the sets cover N>=2. But I'm having trouble stating the problem. In english my proof is:

Each Ai is infinite because you can define the map from N -> Ai[i] just by associating the power. ie for A2 (1->3, 2->9, 3->27...).

The union of all is equal to N>2 because either a) you hit a non-perfect power, and therefore the start of an Ai or b) you are a perfect power and belong to an Ai.

I'm having trouble with pairwise disjoint, but this is my argument:
If the start element (the non-perfect power) of the Ai and Aj are coprime, they must be disjoint. If they aren't coprime but one is even and the other is odd, then they cannot share elements as all powers will be different kinds (odds evens).
If Ai and Aj arent coprime and are both either odd or even, you can make the argument that you can't satisfy the equations for the powers of their prime factorizations.
Ex. 6 and 12 are both non-perfect powers but are both even. but if you try to find 6^n=12^m (written as 2^n*3^n=2^2m*3^m when factorized) then you cannot find n = 2m and n = m except for n=0 which isn't valid.

Sorry for the long post, would love some help though!

[Ruben Van de Velde]

I'm not sure about your idea, but maybe a simpler approach is to set $A_i$ to be the set of numbers whose smallest prime factor (docs#Nat.minFac) is the $i$'th prime

[Daniel Weber]

Here's how I'd state in Lean what you described, although I agree with Ruben Van de Velde that using another partition might be easier (something which should be really easy is partitioning based on the first element of docs#Nat.unpair, for instance)

import Mathlib

/--
Prop stating that a numer is a perfect power.
-/
def IsPower (m : ℕ) := ∃ n k, 1 < k ∧ n ^ k = m


/--
Every number greater than one can be uniquely represented as a power of a number which isn't a perfect power.
-/
lemma utility_lemma (m : ℕ) (hm : 1 < m) : ∃! n : ℕ × ℕ, ¬IsPower n.1 ∧ n.1 ^ n.2 = m := by
  sorry

def nonPerfect : Set ℕ := {n : ℕ | ¬ IsPower n}

def setSeq : ℕ → Set ℕ
| 0 => nonPerfect ∪ {0, 1}
| i + 1 => (· ^ (i + 2)) '' nonPerfect

theorem infinite (i : ℕ) : (setSeq i).Infinite := by
  sorry

theorem covers_ℕ : ⋃ n, setSeq n = Set.univ := by
  sorry

theorem pairwise_disjoint : Set.univ.PairwiseDisjoint setSeq := by
  sorry

[max]

Thanks both! Yeah I really like Rubens solution. Thank you for the starter code