theorem Set.mem_image_of_mem
theorem Set.mem_image_of_mem: ∀ {α : Type u} {β : Type v} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a
theorem Set.mem_image_of_mem
theorem Set.mem_image_of_mem: ∀ {α : Type u} {β : Type v} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a