Moving neighborhoods from one point to another

Stream: Is there code for X?

[Antoine Chambert-Loir]

Is there a more direct way to translate a neighborhood from one point to another (here, in a ring) than doing this :

import Mathlib.Topology.Algebra.Ring.Basic

open Continuous
example {α : Type _} [CommRing α] [TopologicalSpace α] [TopologicalRing α]
  (a b : α) (V : Set α) (hV : V ∈ nhds (a + b)) :
  (Add.add a) ⁻¹' V ∈ nhds b :=  by
  apply continuousAt_def.mp
  apply continuousAt
  apply continuous_add_left _
  exact hV

[Patrick Massot]

A more efficient version is

  rw [(Homeomorph.addLeft a).nhds_eq_comap]
  exact Filter.preimage_mem_comap hV

but there may be an even shorter one

[Patrick Massot]

Actually my answer is a bit silly, going through a much stronger fact. The whole proof term you want is (continuous_add_left a).continuousAt hV

[Patrick Massot]

I was somewhat misled by the number of lines in your solution that suggested a fight.

[Antoine Chambert-Loir]

(deleted)