case zero
R : Type ?u.25159
a : ZMod Nat.zero
⊢ ↑↑a = a

case succ
R : Type ?u.25159
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ ↑↑a = a
n : ℕ
R : Type ?u.25159
a : ZMod n
⊢ ↑↑a = a
cases n
no goals
case zero
R : Type ?u.25159
a : ZMod Nat.zero
⊢ ↑↑a = a
simp [ZMod.cast, ZMod]
case succ
R : Type ?u.25159
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ ↑↑(val a) = a
case succ
R : Type ?u.25159
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ ↑↑a = a
dsimp [ZMod.cast, ZMod]
no goals
case succ
R : Type ?u.25159
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ ↑↑(val a) = a
erw [Int.cast_ofNat, Fin.cast_val_eq_self]