simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq]
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ S n ∈ A
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ ¬S n = z → ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }