awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
a : (‖x‖ / r * (r * ‖x‖⁻¹)) • x = x
⊢ (↑((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
              { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
          ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
              have this := ⋯;
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E))
                  ⋯,
                Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx))) :
      E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx) : E)

Tactic:
simp only [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
a : HSMul.hSMul (α := ℝ) 1 x = x
⊢ (‖x‖ / r * (r * ‖x‖⁻¹)) • x = x

Tactic:
field_simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
⊢ HSMul.hSMul (α := ℝ) 1 x = x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) (sphere 0 r) x
d : ℝ
hd : Membership.mem (γ := Set ℝ) (Ioi 0) d
⊢ 0 < d

Tactic:
rw [mem_Ioi] at hd

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) (sphere 0 r) x
d : ℝ
hd_1 : Membership.mem (γ := Set ℝ) (Ioi 0) d
hd : 0 < d
rw :
  ∀ (hx_1 : ‖x‖ = r) (d : ℝ) (hd : Membership.mem (γ := Set ℝ) (Ioi 0) d) (hd_2 : 0 < d),
    (fun (x : (↑{0}ᶜ : Type u_2)) ↦
          have this := ⋯;
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
            Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
        ((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
              { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
            Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd)) =
      (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
        Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd)
⊢ (fun (x : (↑{0}ᶜ : Type u_2)) ↦
        have this := ⋯;
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
      ((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
            { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd_1)) =
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd_1)

Tactic:
rw [mem_sphere_zero_iff_norm] at hx

Premises used: mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx_1 : Membership.mem (γ := Set E) (sphere 0 r) x
hx : ‖x‖ = r
d : ℝ
hd_1 : Membership.mem (γ := Set ℝ) (Ioi 0) d
hd : 0 < d
⊢ (fun (x : (↑{0}ᶜ : Type u_2)) ↦
        have this := ⋯;
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
      ((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
            { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx_1,
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd_1)) =
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) x hx_1,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) d hd_1)

Tactic:
simp (disch := positivity) [norm_smul, smul_smul, abs_of_pos hd, hx]

Premises used: norm_smul, smul_smul, abs_of_pos
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
⊢ ∀ (x : (↑{0}ᶜ : Type u_2)), ‖(↑x : E)‖ ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
funProp : ∀ (x : (↑{0}ᶜ : Type u_2)), ‖(↑x : E)‖ ≠ 0
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun (x : (↑{0}ᶜ : Type u_2)) ↦
    (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
      Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯)

Tactic:
fun_prop (disch := simp)
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
rw :
  ∀ x ∈ U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V,
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V ∈ 𝓝 x
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
inr :
  ∀
    (this :
      ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
        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))
    (hx₀ : ¬0 < x),
    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)
wlog :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
⊢ 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:
wlog hx₀ : 0 < x generalizing x U
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : ¬0 < x
⊢ x = 0 ∨ 0 < -x

Tactic:
rw [not_lt, le_iff_eq_or_lt, ← neg_pos] at hx₀

Premises used: le_iff_eq_or_lt, neg_pos, not_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : x = 0 ∨ 0 < -x
⊢ 0 < -x

Tactic:
hx₀.resolve_left <| ne_of_mem_of_not_mem hxU hU₀

Premises used: Or.resolve_left, ne_of_mem_of_not_mem
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : x = 0 ∨ 0 < -x
⊢ 0 < -x

Tactic:
exact hx₀.resolve_left <| ne_of_mem_of_not_mem hxU hU₀

Premises used: Or.resolve_left, ne_of_mem_of_not_mem
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : ¬0 < x
⊢ 0 < -x

Tactic:
replace hx₀ : 0 < -x := by
      rw [not_lt, le_iff_eq_or_lt, ← neg_pos] at hx₀
      exact hx₀.resolve_left <| ne_of_mem_of_not_mem hxU hU₀
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : 0 < -x
⊢ 0 ∉ -U

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : 0 < -x
⊢ -x ∈ -U

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
this :
  ∀ {U : Set ℝ} (hU : IsOpen U) (hU₀ : 0 ∉ U) (x : ℝ) (hxU : x ∈ U) (hx₀ : 0 < x),
    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)
hx₀ : 0 < -x
⊢ 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:
specialize this hU.neg (by simpa) (-x) (by simpa) hx₀

Premises used: Neg.neg, IsOpen.neg
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
hx₀ : 0 < -x
this :
  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)
⊢ Neg.neg ⁻¹' (-(U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)) ∈
    𝓝 (x • (↑y : E))

Tactic:
simp only [neg_smul, nhds_neg, Set.neg_smul, Filter.mem_neg] at this

Premises used: neg_smul, nhds_neg, Set.neg_smul, Filter.mem_neg
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
U : Set ℝ
V : Set (↑(sphere 0 r) : Type u_1)
hU : IsOpen U
hU₀ : 0 ∉ U
hV : IsOpen[instTopologicalSpaceSubtype] V
x : ℝ
hxU : x ∈ U
y : { x : E // Membership.mem (γ := Set E) (sphere 0 r) x }
hyV : y ∈ V
hx₀ : 0 < -x
this :
  Neg.neg ⁻¹' (-(U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V)) ∈
    𝓝 (x • (↑y : 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:
simpa using this
-- 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
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
⊢ 0 ≤ r

Tactic:
simpa using norm_nonneg y.1

Premises used: Subtype.val, norm_nonneg
-- 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
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
⊢ 0 < r

Tactic:
have hr₀ : 0 < r := lt_of_le_of_ne (by simpa using norm_nonneg y.1) hr.symm
-- 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
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
hr₀ : 0 < r
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x

Tactic:
hx₀

Premises used: Set.Ioi, Set.Mem, setOf
-- 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
x : ℝ
hxU : x ∈ U
hx₀ : 0 < x
hr₀ : 0 < r
lift :
  ∀ (x : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }) (hxU : (↑x : ℝ) ∈ U),
    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)
⊢ 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:
lift x to Ioi (0 : ℝ) using hx₀

Premises used: Set.Ioi, OfNat.ofNat
-- 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
⊢ SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈ 𝓝 (y, x)

Tactic:
have : V ×ˢ (Ioi (0 : ℝ) ↓∩ U) ∈ 𝓝 (y, x) :=
    prod_mem_nhds (hV.mem_nhds hyV) (hU.preimage_val.mem_nhds hxU)
-- 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 : SProd.sprod (β := Set (↑(Ioi 0) : Type)) V (Ioi 0 ↓∩ U) ∈ 𝓝 (y, x)
⊢ 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))

Tactic:
replace := image_mem_map (m := Subtype.val ∘ (homeomorphSphereProd E r hr₀).symm) this
-- 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 :
  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))
h :
  ∀ (a : E),
    Membership.mem (γ := Set 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))
        a →
      a ∈ U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
⊢ 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:
filter_upwards [this]
-- 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 :
  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))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
h :
  (↑(a, b).2 : ℝ) • (↑(a, b).1 : E) ∈
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
⊢ 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))
      (a, b) ∈
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V

Tactic:
rw [Function.comp_apply, homeomorphSphereProd_symm_apply_coe]

Premises used: homeomorphSphereProd_symm_apply_coe, Function.comp_apply
-- 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 :
  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))
a : (↑(sphere 0 r) : Type u_1)
b : (↑(Ioi 0) : Type)
ha : (a, b).1 ∈ V
hb : Membership.mem (γ := Set (↑(Ioi 0) : Type)) (Ioi 0 ↓∩ U) (a, b).2
h : (↑(a, b).2 : ℝ) ∈ U
h₁ : (↑(a, b).1 : E) ∈ Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V
⊢ (↑(a, b).2 : ℝ) • (↑(a, b).1 : E) ∈
    U • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) '' V

Tactic:
apply Set.smul_mem_smul

Premises used: Set.smul_mem_smul