n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = n
n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * val a = n
rw [neg_eq_iff_add_eq_zero, ← two_mul]
case zero
a : ZMod Nat.zero
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = Nat.zero

case succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = Nat.succ n✝
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = n
cases n
case succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ Nat.succ n✝ ∣ 2 * val a ↔ a = 0 ∨ 2 * val a = Nat.succ n✝
case succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = Nat.succ n✝
conv_lhs =>
  rw [← a.nat_cast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, nat_cast_zmod_eq_zero_iff_dvd]
case succ.mp
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ Nat.succ n✝ ∣ 2 * val a → a = 0 ∨ 2 * val a = Nat.succ n✝

case succ.mpr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝ → Nat.succ n✝ ∣ 2 * val a
case succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ Nat.succ n✝ ∣ 2 * val a ↔ a = 0 ∨ 2 * val a = Nat.succ n✝
constructor
case zero
a : ZMod Nat.zero
⊢ 2 = 0 ∨ a = 0 ↔ a = 0 ∨ 2 = 0 ∨ a = 0
case zero
a : ZMod Nat.zero
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * val a = Nat.zero
erw [@mul_eq_zero ℤ, @mul_eq_zero ℕ, val_eq_zero]
no goals
case zero
a : ZMod Nat.zero
⊢ 2 = 0 ∨ a = 0 ↔ a = 0 ∨ 2 = 0 ∨ a = 0
exact
  ⟨fun h => h.elim (by simp) Or.inl, fun h =>
    Or.inr (h.elim id fun h => h.elim (by simp) id)⟩
no goals
a : ZMod Nat.zero
h : 2 = 0 ∨ a = 0
⊢ 2 = 0 → a = 0 ∨ 2 = 0 ∨ a = 0
simp
no goals
a : ZMod Nat.zero
h✝ : a = 0 ∨ 2 = 0 ∨ a = 0
h : 2 = 0 ∨ a = 0
⊢ 2 = 0 → a = 0
simp
case succ.mp.intro
n✝ : ℕ
a : ZMod (Nat.succ n✝)
m : ℕ
he : 2 * val a = Nat.succ n✝ * m
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
case succ.mp
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ Nat.succ n✝ ∣ 2 * val a → a = 0 ∨ 2 * val a = Nat.succ n✝
rintro ⟨m, he⟩
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.zero
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝

case succ.mp.intro.succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
m : ℕ
he : 2 * val a = Nat.succ n✝ * Nat.succ m
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
case succ.mp.intro
n✝ : ℕ
a : ZMod (Nat.succ n✝)
m : ℕ
he : 2 * val a = Nat.succ n✝ * m
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
cases' m with m
case succ.mp.intro.succ.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.succ Nat.zero
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝

case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝¹
case succ.mp.intro.succ
n✝ : ℕ
a : ZMod (Nat.succ n✝)
m : ℕ
he : 2 * val a = Nat.succ n✝ * Nat.succ m
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
cases m
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 2 * Nat.succ n✝¹ ≤ 2 * val a
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝¹
refine' (a.val_lt.not_le <| Nat.le_of_mul_le_mul_left _ zero_lt_two).elim
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ Nat.succ n✝¹ * 2 ≤ Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 2 * Nat.succ n✝¹ ≤ 2 * val a
rw [he, mul_comm]
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 2 ≤ Nat.succ (Nat.succ n✝)
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ Nat.succ n✝¹ * 2 ≤ Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
apply Nat.mul_le_mul_left
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 0 ≤ n✝
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 2 ≤ Nat.succ (Nat.succ n✝)
erw [Nat.succ_le_succ_iff, Nat.succ_le_succ_iff]
no goals
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (Nat.succ n✝¹)
n✝ : ℕ
he : 2 * val a = Nat.succ n✝¹ * Nat.succ (Nat.succ n✝)
⊢ 0 ≤ n✝
simp
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 = 0 ∨ val a = 0
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.zero
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
erw [MulZeroClass.mul_zero, mul_eq_zero] at he
case succ.mp.intro.zero.inr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : val a = 0
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 = 0 ∨ val a = 0
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
rcases he with (⟨⟨⟩⟩ | he)
no goals
case succ.mp.intro.zero.inr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : val a = 0
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
exact Or.inl (a.val_eq_zero.1 he)
case succ.mp.intro.succ.zero.h
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.succ Nat.zero
⊢ 2 * val a = Nat.succ n✝
case succ.mp.intro.succ.zero
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.succ Nat.zero
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝
right
no goals
case succ.mp.intro.succ.zero.h
n✝ : ℕ
a : ZMod (Nat.succ n✝)
he : 2 * val a = Nat.succ n✝ * Nat.succ Nat.zero
⊢ 2 * val a = Nat.succ n✝
rwa [show Nat.succ Nat.zero = 1 from rfl, mul_one] at he
case succ.mpr.inl
n✝ : ℕ
⊢ Nat.succ n✝ ∣ 2 * val 0

case succ.mpr.inr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
h : 2 * val a = Nat.succ n✝
⊢ Nat.succ n✝ ∣ 2 * val a
case succ.mpr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ a = 0 ∨ 2 * val a = Nat.succ n✝ → Nat.succ n✝ ∣ 2 * val a
rintro (rfl | h)
case succ.mpr.inl
n✝ : ℕ
⊢ Nat.succ n✝ ∣ 0
case succ.mpr.inl
n✝ : ℕ
⊢ Nat.succ n✝ ∣ 2 * val 0
rw [val_zero, MulZeroClass.mul_zero]
no goals
case succ.mpr.inl
n✝ : ℕ
⊢ Nat.succ n✝ ∣ 0
apply dvd_zero
no goals
case succ.mpr.inr
n✝ : ℕ
a : ZMod (Nat.succ n✝)
h : 2 * val a = Nat.succ n✝
⊢ Nat.succ n✝ ∣ 2 * val a
rw [h]