rcases heq hne with ⟨a, ⟨h, 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 : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
case intro.intro
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✝ : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
a : α
h : a ∈ N0
heq : n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m