simp [A, Set.ext_iff] at heq
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ mul (z, x) = z
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ∀ (x : α), (∃ (x_1 : x ∈ N0), mul (z, { val := x, property := (_ : x ∈ N0) }) = z) ↔ x ∈ N0
⊢ mul (z, x) = z