simp only [ite_true, and_true, hn]
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
⊢ ((∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0) ∧
    (if i = i then k else if i = i' then r else 1) = k
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
⊢ (∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0