have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n _
  simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq]
  intro _
  use n
  simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const]
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∃ m, n = S m
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ ∃ m, n = S m