Eq finsum quotient out of bij On

lemma eq_finsum_quotient_out_of_bijOn' (a : fixedPoints V A)    {X : Set (G ⧸ V)}    {s : Set G} (hs : s.BijOn (QuotientGroup.mk : G → G ⧸ V) X) :    ∑ᶠ g ∈ s, g • (a : A) = ∑ᶠ g ∈ Quotient.out '' X, g • (a : A) := by  let e (g : G) : G := Quotient.out (QuotientGroup.mk g : G ⧸ V)  have he₀ : Set.BijOn e s (Quotient.out '' X) := by    refine Set.BijOn.comp ?_ hs    exact Set.InjOn.bijOn_image <| Set.injOn_of_injective Quotient.out_injective  have he₁ : ∀ g ∈ s, g • (a : A) = (Quotient.out (QuotientGroup.mk g : G ⧸ V)) • a := by    intro g hgs    obtain ⟨v, hv⟩ := QuotientGroup.mk_out_eq_mul V g    rw [hv, mul_smul, (show (v : G) • (a : A) = a from a.2 v)]  exact finsum_mem_eq_of_bijOn e he₀ he₁