case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod Nat.zero
⊢ (↑a).fst = ↑a

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).fst = ↑a
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ (↑a).fst = ↑a
cases n
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).fst = ↑a
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod Nat.zero
⊢ (↑a).fst = ↑a

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).fst = ↑a
. rfl
no goals
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).fst = ↑a
. simp [ZMod.cast]
no goals
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod Nat.zero
⊢ (↑a).fst = ↑a
rfl
no goals
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (Nat.succ n✝)
⊢ (↑a).fst = ↑a
simp [ZMod.cast]