case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod Nat.zero
k : ZMod Nat.zero
⊢ ↑f ↑k = k

case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (Nat.succ n✝)
k : ZMod (Nat.succ n✝)
⊢ ↑f ↑k = k
n : ℕ
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod n
k : ZMod n
⊢ ↑f ↑k = k
cases n
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (Nat.succ n✝)
k : ZMod (Nat.succ n✝)
⊢ ↑f ↑k = k
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod Nat.zero
k : ZMod Nat.zero
⊢ ↑f ↑k = k

case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (Nat.succ n✝)
k : ZMod (Nat.succ n✝)
⊢ ↑f ↑k = k
. dsimp [ZMod, ZMod.cast] at f k ⊢; simp
no goals
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (Nat.succ n✝)
k : ZMod (Nat.succ n✝)
⊢ ↑f ↑k = k
. dsimp [ZMod, ZMod.cast] at f k ⊢
  erw [map_natCast, Fin.cast_val_eq_self]
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ℤ
k : ℤ
⊢ ↑f ↑k = k
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ZMod Nat.zero
k : ZMod Nat.zero
⊢ ↑f ↑k = k
dsimp [ZMod, ZMod.cast] at f k ⊢
no goals
case zero
R : Type u_1
inst✝ : Ring R
f : R →+* ℤ
k : ℤ
⊢ ↑f ↑k = k
simp
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* Fin (n✝ + 1)
k : Fin (n✝ + 1)
⊢ ↑f ↑(val k) = k
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* ZMod (Nat.succ n✝)
k : ZMod (Nat.succ n✝)
⊢ ↑f ↑k = k
dsimp [ZMod, ZMod.cast] at f k ⊢
no goals
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
f : R →+* Fin (n✝ + 1)
k : Fin (n✝ + 1)
⊢ ↑f ↑(val k) = k
erw [map_natCast, Fin.cast_val_eq_self]