n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ ↑0 = 0
delta ZMod.cast
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.zero with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0

case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.succ n✝ with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
n : ℕ
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) n with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
cases n
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.succ n✝ with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.zero with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0

case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.succ n✝ with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
. exact Int.cast_zero
no goals
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.succ n✝ with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
. simp
no goals
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.zero with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
exact Int.cast_zero
no goals
case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) Nat.succ n✝ with
      | 0 => Int.cast
      | Nat.succ n => fun i => ↑(val i))
      0 =
    0
simp