simp [A, Set.ext_iff] at heq
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ ∃ 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
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0),
        ¬{ val := x, property := (_ : x ∈ N0) } = z →
          ∃ a, ∃ (b : a ∈ N0), { val := x, property := (_ : x ∈ N0) } = S { val := a, property := b }) ↔
      x ∈ N0
⊢ ∃ m, n = S m