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