case zero
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD Nat.zero]

case succ
a b n✝ : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD Nat.succ n✝]
n a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD n]
cases n
no goals
case zero
a b : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD Nat.zero]
simp [Nat.ModEq, Int.coe_nat_inj', Nat.mod_zero]
case succ
a b n✝ : ℕ
⊢ ↑↑a = ↑↑b ↔ val ↑a = val ↑b
case succ
a b n✝ : ℕ
⊢ ↑a = ↑b ↔ a ≡ b [MOD Nat.succ n✝]
rw [Fin.ext_iff, Nat.ModEq, ← val_nat_cast, ← val_nat_cast]
no goals
case succ
a b n✝ : ℕ
⊢ ↑↑a = ↑↑b ↔ val ↑a = val ↑b
exact Iff.rfl