∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {l : Filter α}
  {m : α → G} {a : G}, Filter.Tendsto (fun x => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)