M : Type ?u.159604
α : Type u_1
β : Type ?u.159610
Γ : Type ?u.159613
inst✝⁶ : Group Γ
T : Type ?u.159619
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hs : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
hc : c ≠ 0
⊢ ∃ t, t ⊆ c • s ∧ IsOpen t ∧ c • x ∈ t
M : Type ?u.159604
α : Type u_1
β : Type ?u.159610
Γ : Type ?u.159613
inst✝⁶ : Group Γ
T : Type ?u.159619
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hs : s ∈ 𝓝 x
hc : c ≠ 0
⊢ c • s ∈ 𝓝 (c • x)
rw [mem_nhds_iff] at hs ⊢
case intro.intro.intro
M : Type ?u.159604
α : Type u_1
β : Type ?u.159610
Γ : Type ?u.159613
inst✝⁶ : Group Γ
T : Type ?u.159619
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
U : Set α
hs' : U ⊆ s
hU : IsOpen U
hU' : x ∈ U
⊢ ∃ t, t ⊆ c • s ∧ IsOpen t ∧ c • x ∈ t
M : Type ?u.159604
α : Type u_1
β : Type ?u.159610
Γ : Type ?u.159613
inst✝⁶ : Group Γ
T : Type ?u.159619
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hs : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t
hc : c ≠ 0
⊢ ∃ t, t ⊆ c • s ∧ IsOpen t ∧ c • x ∈ t
obtain ⟨U, hs', hU, hU'⟩ := hs
no goals
case intro.intro.intro
M : Type ?u.159604
α : Type u_1
β : Type ?u.159610
Γ : Type ?u.159613
inst✝⁶ : Group Γ
T : Type ?u.159619
inst✝⁵ : TopologicalSpace T
inst✝⁴ : MulAction Γ T
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
c : G₀
s : Set α
x : α
hc : c ≠ 0
U : Set α
hs' : U ⊆ s
hU : IsOpen U
hU' : x ∈ U
⊢ ∃ t, t ⊆ c • s ∧ IsOpen t ∧ c • x ∈ t
exact ⟨c • U, Set.smul_set_mono hs', hU.smul₀ hc, Set.smul_mem_smul_set hU'⟩