-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set (↑(sphere 0 r) : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }
hxU : (↑x : ℝ) ∈ U
this :
  Membership.mem (γ := Filter E)
    (map
      (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
      (𝓝 (y, x)))
    (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
        (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
        (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
          (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
      SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))
rw :
  ∀
    (this :
      Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
          SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈
        𝓝 ((↑(y, x).2 : ℝ) • (↑(y, x).1 : E))),
    Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
      (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)
h :
  ∀
    (this :
      Membership.mem (γ := Filter E)
        (𝓝[{0}ᶜ]
          (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
                  (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
                (y, x)) :
            E))
        (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
          SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ
ha :
  ∀
    (this :
      Membership.mem (γ := Filter E)
        (𝓝[{0}ᶜ]
          (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
                  (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
                (y, x)) :
            E))
        (Function.comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            (⇑(Homeomorph.symm (homeomorphSphereProd E r hr₀)) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)) ''
          SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U))),
    Membership.mem (γ := Set E) {0}ᶜ
      (↑((Homeomorph.symm (homeomorphSphereProd E r hr₀) :
              (a : (↑(sphere 0 r) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
            (y, x)) :
        E)
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (x1 : ℝ) (x2 : E) ↦ x1 • x2) (↑x : ℝ) (↑y : E)))
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)

Tactic:
rw [← Filter.map_map, (homeomorphSphereProd _ r hr₀).symm.map_nhds_eq,
    map_nhds_subtype_val, IsOpen.nhdsWithin_eq, homeomorphSphereProd_symm_apply_coe] at this

Premises used: IsOpen.nhdsWithin_eq, homeomorphSphereProd, Homeomorph.map_nhds_eq, Filter.map_map, homeomorphSphereProd_symm_apply_coe, Homeomorph.symm, map_nhds_subtype_val