simp only [Set.mem_setOf_eq] at hel
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (S x, S n) = S (plus (x, S n))
x y : ↑N0
A : Set ↑N0 := {y | plus (S x, y) = S (plus (x, y))}
hzmem : z ∈ A
n : ↑N0
hel : plus (S x, n) = S (plus (x, n))
⊢ plus (S x, S n) = S (plus (x, S n))