simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0), plus (z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔
    ↑x ∈ N0
⊢ plus (z, x) = x
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (z, x) = x
⊢ plus (z, x) = x