case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑(val z) + ↑p * k

case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑(val z) + ↑p * k) → ↑n = z
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = ↑(val z) + ↑p * k
constructor
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ ∃ k, n = ↑(val ↑n) + ↑p * k
case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑(val z) + ↑p * k
rintro rfl
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(val ↑n) + ↑p * (n / ↑p)
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ ∃ k, n = ↑(val ↑n) + ↑p * k
refine' ⟨n / p, _⟩
no goals
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(val ↑n) + ↑p * (n / ↑p)
rw [val_int_cast, Int.emod_add_ediv]
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑(↑(val z) + ↑p * k) = z
case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑(val z) + ↑p * k) → ↑n = z
rintro ⟨k, rfl⟩
no goals
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑(↑(val z) + ↑p * k) = z
rw [Int.cast_add, Int.cast_mul, Int.cast_ofNat, Int.cast_ofNat, nat_cast_val,
  ZMod.nat_cast_self, MulZeroClass.zero_mul, add_zero, cast_id]