-- Mathlib/Data/ZMod/Basic.lean
theorem neg_eq_self_iff {n : ℕ} (a : ZMod n) : -a = a ↔ a = 0 ∨ 2 * a.val = n

Proof state:
a : ZMod 0
h : 2 = 0 ∨ a = 0
⊢ 2 = 0 → a = 0 ∨ 2 = 0 ∨ a = 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
case succ.mpr
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1 → n✝ + 1 ∣ 2 * a.val

Tactic:
rintro (rfl | h)

Result:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * val 0

case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ 2 * a.val

Proof state:
n : ℕ
a : ZMod n
⊢ -a = a ↔ a = 0 ∨ 2 * a.val = n

Tactic:
rw [neg_eq_iff_add_eq_zero, ← two_mul]

Result:
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n

Proof state:
case zero
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0

Tactic:
rw [@mul_eq_zero ℤ, @mul_eq_zero ℕ, val_eq_zero]

Result:
case zero
a : ZMod 0
⊢ 2 = 0 ∨ a = 0 ↔ a = 0 ∨ 2 = 0 ∨ a = 0

Proof state:
case succ.mp.intro.succ
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * (m + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
cases m

Result:
case succ.mp.intro.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝¹ + 1

Proof state:
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝¹ + 1

Tactic:
refine (a.val_lt.not_le <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim

Result:
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 * (n✝¹ + 1) ≤ 2 * a.val

Proof state:
case succ.mp.intro
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * m
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
rcases m with - | m

Result:
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

case succ.mp.intro.succ
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * (m + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Proof state:
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 ≤ n✝ + 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
rw [mul_zero, mul_eq_zero] at he

Result:
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Proof state:
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ (n✝¹ + 1) * 2 ≤ (n✝¹ + 1) * (n✝ + 1 + 1)

Tactic:
apply Nat.mul_le_mul_left

Result:
case succ.mp.intro.succ.succ.h
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 ≤ n✝ + 1 + 1

Proof state:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
constructor

Result:
case succ.mp
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val → a = 0 ∨ 2 * a.val = n✝ + 1

case succ.mpr
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1 → n✝ + 1 ∣ 2 * a.val

Proof state:
case zero
a : ZMod 0
⊢ 2 = 0 ∨ a = 0 ↔ a = 0 ∨ 2 = 0 ∨ a = 0

Tactic:
exact
  ⟨fun h => h.elim (by simp) Or.inl, fun h =>
    Or.inr (h.elim id fun h => h.elim (by simp) id)⟩

Result:
no goals

Proof state:
case succ.mp.intro.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
right

Result:
case succ.mp.intro.succ.zero.h
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ 2 * a.val = n✝ + 1

Proof state:
case succ.mp.intro.succ.zero.h
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ 2 * a.val = n✝ + 1

Tactic:
rwa [show 0 + 1 = 1 from rfl, mul_one] at he

Result:
no goals

Proof state:
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n

Tactic:
cases n

Result:
case zero
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0

case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Proof state:
case succ.mp
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val → a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
rintro ⟨m, he⟩

Result:
case succ.mp.intro
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * m
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Proof state:
case succ.mp.intro.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
rcases he with (⟨⟨⟩⟩ | he)

Result:
case succ.mp.intro.zero.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
he : a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Proof state:
case succ.mp.intro.zero.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
he : a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
exact Or.inl (a.val_eq_zero.1 he)

Result:
no goals

Proof state:
a : ZMod 0
h✝ : a = 0 ∨ 2 = 0 ∨ a = 0
h : 2 = 0 ∨ a = 0
⊢ 2 = 0 → a = 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
conv_lhs =>
  rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_zmod_eq_zero_iff_dvd]

Result:
case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ n✝ + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Proof state:
case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ 2 * a.val

Tactic:
rw [h]

Result:
no goals

Proof state:
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 * (n✝¹ + 1) ≤ 2 * a.val

Tactic:
rw [he, mul_comm]

Result:
case succ.mp.intro.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ (n✝¹ + 1) * 2 ≤ (n✝¹ + 1) * (n✝ + 1 + 1)

Proof state:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * val 0

Tactic:
rw [val_zero, mul_zero]

Result:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 0