@[simp]

theorem Set.mul_mem_smul_set_iff {α : Type u_1} [Group α] (a : α) {b : α} {s : Set α} : a * b ∈ a • s ↔ b ∈ s

@[simp]

theorem Set.add_mem_vadd_set_iff {α : Type u_1} [AddGroup α] (a : α) {b : α} {s : Set α} : a + b ∈ a +ᵥ s ↔ b ∈ s