simp only [ge_iff_le, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply,
  mul_ite, mul_one, mul_zero, Function.update_same, add_right_inj, ite_eq_left_iff, if_true] at h
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1) k =
    ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1) k
⊢ j = k
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : ¬k = j → False
⊢ j = k