intro j hj
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
⊢ ∀ x ∈ (univ.erase i).erase i', (if x = i then k else if x = i' then r else 1) = 1
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 ∈ (univ.erase i).erase i'
⊢ (if j = i then k else if j = i' then r else 1) = 1