∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : ContinuousConstVAdd G α] (γ : G),
  Homeomorph.vadd γ = { toEquiv := AddAction.toPerm γ, continuous_toFun := ⋯, continuous_invFun := ⋯ }