proving union of sets is equal to \N

Stream: new members

[max]

def IsPerfectPower (m : ℕ) := ∃ n k, 1 < k ∧ n ^ k = m
def Perfect : Set ℕ := {n : ℕ | IsPerfectPower n}
def nonPerfect : Set ℕ := {n : ℕ | ¬IsPerfectPower n}
theorem n_is_perfect_or_not (n : ℕ) : (IsPerfectPower n ∨ ¬IsPerfectPower n) := by
  apply Classical.em

theorem covers_n : Perfect ∪ nonPerfect = ℕ := by
  unfold Perfect nonPerfect
  sorry

I was able to prove that for any n: N, it is either a perfect power or not by the law of the excluded middle.
I want to prove basically the same, but showing that the union of the non perfect and perfect naturals is equal to all the naturals.

The type of Perfect \un nonPerfect is Set \N, but N is not Set N, how should I approach this?
Thanks again, I am really enjoying being on this zulip. Everyone has been so helpful

[Floris van Doorn]

The element of Set ℕ that consists of all natural numbers is spelled Set.univ (or ⊤), not ℕ.

[Notification Bot]

A message was moved here from #lean4 > proving union of sets is equal to \N by Floris van Doorn.

[Floris van Doorn]

@max this is a possible way to prove this

import Mathlib.Tactic

def IsPerfectPower (m : ℕ) := ∃ n k, 1 < k ∧ n ^ k = m
def Perfect : Set ℕ := {n : ℕ | IsPerfectPower n}
def nonPerfect : Set ℕ := {n : ℕ | ¬IsPerfectPower n}
theorem n_is_perfect_or_not (n : ℕ) : (IsPerfectPower n ∨ ¬IsPerfectPower n) := by
  apply Classical.em

theorem covers_n : Perfect ∪ nonPerfect = Set.univ := by
  unfold Perfect nonPerfect
  ext n
  simp
  exact n_is_perfect_or_not n

[Floris van Doorn]

Also, for next time: please list your imports (see #mwe )

[Floris van Doorn]

I recommend that you read Section 4.1 of Mathematics in Lean: https://leanprover-community.github.io/mathematics_in_lean/C04_Sets_and_Functions.html

[max]

thanks a lot Floris!