rw [←Finset.mul_prod_erase (a:=i) (h:=mem_univ _),
  ←Finset.mul_prod_erase (a:= i')]
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
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
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0

case h.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' ∈ univ.erase i