case zero
m : ℕ
inst✝ : NeZero zero
k : Fin zero
⊢ k * 1 = k

case succ
m n : ℕ
inst✝ : NeZero (Nat.succ n)
k : Fin (Nat.succ n)
⊢ k * 1 = k
n m : ℕ
inst✝ : NeZero n
k : Fin n
⊢ k * 1 = k
cases' n with n
case succ.zero
m : ℕ
inst✝ : NeZero (Nat.succ zero)
k : Fin (Nat.succ zero)
⊢ k * 1 = k

case succ.succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ (Nat.succ n✝))
k : Fin (Nat.succ (Nat.succ n✝))
⊢ k * 1 = k
case succ
m n : ℕ
inst✝ : NeZero (Nat.succ n)
k : Fin (Nat.succ n)
⊢ k * 1 = k
cases n
no goals
case succ.succ
m n✝ : ℕ
inst✝ : NeZero (Nat.succ (Nat.succ n✝))
k : Fin (Nat.succ (Nat.succ n✝))
⊢ k * 1 = k
simp [eq_iff_veq, mul_def, mod_eq_of_lt (is_lt k)]
no goals
case zero
m : ℕ
inst✝ : NeZero zero
k : Fin zero
⊢ k * 1 = k
simp
no goals
case succ.zero
m : ℕ
inst✝ : NeZero (Nat.succ zero)
k : Fin (Nat.succ zero)
⊢ k * 1 = k
simp [fin_one_eq_zero]