The lemma holds only if you add the assumption inj f
stating that f
is injective. The lemma then follows from the library lemma setprod_reindex_id
, which can be found using the command find_theorems setprod image
.
setprod_reindex_id [unfolded id_def]
gives you a generalized version of the lemma you asked for.