no goals
M : Type ?u.30275
α : Type u_2
β : Type u_1
G : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun x => c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)
simpa only [inv_smul_smul] using h.const_smul c⁻¹