Multipliable.congr for almost equal functions

Stream: Is there code for X?

[Xavier Roblot]

There is docs#Multipliable.congr, but the following more general version seems to be missing:

import Mathlib.Topology.Algebra.InfiniteSum.Group

open Filter

theorem Multipliable.congr' {α β : Type*} [CommGroup α] [TopologicalSpace α] [TopologicalGroup α]
    {f g : β → α} (hf : Multipliable f) (hfg : ∀ᶠ b in cofinite, f b = g b) :
    Multipliable g :=
  hfg.multipliable_compl_iff.mp <| (hfg.multipliable_compl_iff.mpr hf).congr (by simp)

[Xavier Roblot]

#18561