Convert `z ∣ ` to divisor list

Stream: new members

[Li Xuanji]

Are there lemma-free proofs for either of these theorems?

import Mathlib

lemma ndvd_two_then (z : ℕ) (hz : z ∣ 2) : z = 1 ∨ z = 2 := by
  have : z ∈ Nat.divisors 2 := by grind [Nat.mem_divisors]
  rw [show Nat.divisors 2 = {1, 2} by rfl] at this
  grind

lemma zdvd_two_then (z : ℤ) (hz : z ∣ 2) : z = 1 ∨ z = -1 ∨ z = 2 ∨ z = -2 := by
  have : (Int.natAbs z) ∣ 2 := by
    rw [← Int.ofNat_dvd_right]
    norm_num
    exact hz
  have : (Int.natAbs z) ∈ Nat.divisors 2 := by grind [Nat.mem_divisors]
  simp [show Nat.divisors 2 = {1, 2} by rfl] at this
  grind

(failing that, any way to make them shorter?)

[Yongxi Lin (Aaron)]

My attempt:

import Mathlib

lemma ndvd_two_then (z : ℕ) (hz : z ∣ 2) : z = 1 ∨ z = 2 := by
  have : z ∈ Nat.divisors 2 := by grind
  simpa [show Nat.divisors 2 = {1, 2} by rfl] using this

lemma zdvd_two_then (z : ℤ) (hz : z ∣ 2) : z = 1 ∨ z = -1 ∨ z = 2 ∨ z = -2 := by
  have : (Int.natAbs z) ∣ 2 := by simpa [← Int.ofNat_dvd_right] using hz
  grind [ndvd_two_then (Int.natAbs z) this]

[Eric Wieser]

We have another thread about this somewhere

[Li Xuanji]

Ah, I found the thread, which taught me about the divisors_ofNat simproc.

import Mathlib

lemma ndvd_two_then (z : ℕ) (hz : z ∣ 2) : z = 1 ∨ z = 2 := by
  have : z ∈ Nat.divisors 2 := by grind [Nat.mem_divisors]
  simp_all

I think there is a problem that Nat.mem_divisors (marked as @simp) simplifies Nat.divisors 2 to z ∣ 2, but the divisors_ofNat simproc fires on Nat.divisors 2 but not z ∣ 2