obtain ⟨i', hi_ne⟩ := exists_ne i
case a.mpr.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
case a.mpr.intro.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k