have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  rw [zmul]
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
⊢ mul (z, x) = z
x : ↑N0
A : Set ↑N0 := {x | mul (z, x) = z}
hzmem : z ∈ A
⊢ mul (z, x) = z