no goals
α : Type u_4
β : Type u_3
γ : Type ?u.300313
ι : Type ?u.300316
M : Type u_1
M' : Type ?u.300322
N : Type u_2
P : Type ?u.300328
G : Type ?u.300331
H : Type ?u.300334
R : Type ?u.300337
S : Type ?u.300340
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α → β
l : β →₀ M
g : β → M → N
hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support
⊢ ∑ x in preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)),
      g (f x)
        (↑{ support := preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)), toFun := fun a => ↑l (f a),
              mem_support_toFun :=
                (_ :
                  ∀ (a : α),
                    a ∈ preimage l.support f (_ : Set.InjOn f (f ⁻¹' ↑l.support)) ↔ (fun a => ↑l (f a)) a ≠ 0) }
          x) =
    ∑ x in l.support, g x (↑l x)
exact Finset.sum_preimage_of_bij f _ hf fun x => g x (l x)