-- Mathlib/Data/ZMod/Units.lean
/-- Any element of `ZMod N` has the form `u * d` where `u` is a unit and `d` is a divisor of `N`. -/
lemma eq_unit_mul_divisor {N : ℕ} (a : ZMod N) :
    ∃ d : ℕ, d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * d

Proof state:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ IsUnit ↑a₀

Tactic:
refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)

Result:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ IsCoprime ↑a₀ ↑N₀

Proof state:
N : ℕ
a : ZMod N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
rcases eq_or_ne N 0 with rfl | hN

Result:
case inl
a : ZMod 0
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (unitsMap ⋯) u = hu₀.unit
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
rw [unitsMap_def, ← Units.eq_iff, Units.coe_map, IsUnit.unit_spec, MonoidHom.coe_coe] at hu

Result:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ IsCoprime ↑a₀ ↑N₀

Tactic:
obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩

Result:
case intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d = ↑a.val * p + ↑N * q
⊢ IsCoprime ↑a₀ ↑N₀

Proof state:
case inr.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
obtain ⟨u, hu⟩ := (ZMod.unitsMap_surjective (⟨d, mul_comm d N₀ ▸ hN₀⟩ : N₀ ∣ N)) hu₀.unit

Result:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (unitsMap ⋯) u = hu₀.unit
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inl.inr.inl
a : ℤ
ha : a ≠ 0
h : a < 0
⊢ IsUnit a.sign

Tactic:
simp only [Int.sign_eq_neg_one_of_neg h, IsUnit.neg_iff, isUnit_one]

Result:
no goals

Proof state:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
have hd : d ≠ 0 := Nat.gcd_ne_zero_right hN

Result:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ a = ↑u * ↑d

Tactic:
rw [← ZMod.natCast_zmod_val a, ← ZMod.natCast_zmod_val u.1, ha₀, ← Nat.cast_mul,
  ZMod.natCast_eq_natCast_iff, mul_comm _ d, Nat.ModEq]

Result:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ d * a₀ % N = d * (↑u).val % N

Proof state:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ a₀ % N₀ = (↑u).val % N₀

Tactic:
rw [← Nat.ModEq, ← ZMod.natCast_eq_natCast_iff, ← hu, natCast_val, castHom_apply]

Result:
no goals

Proof state:
case inl.inr
a : ℤ
ha : a ≠ 0
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
refine ⟨a.natAbs, dvd_zero _, Int.sign a, ?_, (Int.sign_mul_natAbs a).symm⟩

Result:
case inl.inr
a : ℤ
ha : a ≠ 0
⊢ IsUnit a.sign

Proof state:
case intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d = ↑a.val * p + ↑N * q
⊢ IsCoprime ↑a₀ ↑N₀

Tactic:
rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm,
  mul_comm _ p, mul_comm _ q] at hpq

Result:
case intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d * (p * ↑a₀ + q * ↑N₀) = ↑d
⊢ IsCoprime ↑a₀ ↑N₀

Proof state:
case inl.inl

⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ 0 = u * ↑d

Tactic:
refine ⟨0, dvd_zero _, 1, isUnit_one, by rw [Nat.cast_zero, mul_zero]⟩

Result:
no goals

Proof state:
case inl.inr
a : ℤ
ha : a ≠ 0
⊢ IsUnit a.sign

Tactic:
rcases lt_or_gt_of_ne ha with h | h

Result:
case inl.inr.inl
a : ℤ
ha : a ≠ 0
h : a < 0
⊢ IsUnit a.sign

case inl.inr.inr
a : ℤ
ha : a ≠ 0
h : a > 0
⊢ IsUnit a.sign

Proof state:
case intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d * (p * ↑a₀ + q * ↑N₀) = ↑d
⊢ IsCoprime ↑a₀ ↑N₀

Tactic:
exact ⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩

Result:
no goals

Proof state:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
let d := a.val.gcd N

Result:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inl
a : ℤ
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Result:
case inl.inl

⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ 0 = u * ↑d

case inl.inr
a : ℤ
ha : a ≠ 0
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inl
a : ZMod 0
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
change ℤ at a

Result:
case inl
a : ℤ
⊢ ∃ d, d ∣ 0 ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
refine ⟨u.val, u.isUnit, ?_⟩

Result:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ a = ↑u * ↑d

Proof state:
case inr.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
obtain ⟨N₀, (hN₀ : _ = d * _)⟩ := a.val.gcd_dvd_right N

Result:
case inr.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inr.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
refine ⟨d, ⟨N₀, hN₀⟩, ?_⟩

Result:
case inr.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d