∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι → κ),
  Function.Injective e →
    ∀ (f : ι → M) (g : κ → M), (∀ i ∉ Set.range e, g i = 1) → (∀ (i : ι), f i = g (e i)) → ∏ i, f i = ∏ j, g j