rw [if_neg hj.1, if_neg hj.2]
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : ¬j = i' ∧ ¬j = i
⊢ (if j = i then k else if j = i' then r else 1) = 1
no goals