theorem Set.mem_smul_iff_inv_smul_mem {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {s : Set G} {t : Set X} {x : X} : x ∈ s • t ↔ ∃ a ∈ s, a⁻¹ • x ∈ t

theorem Set.mem_vadd_iff_neg_vadd_mem {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] {s : Set G} {t : Set X} {x : X} : x ∈ s +ᵥ t ↔ ∃ a ∈ s, -a +ᵥ x ∈ t