simp only [tw, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Subtype.mk.injEq] at h
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : tw n d j = tw n d k
⊢ j = k
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 =
    (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1
⊢ j = k