Image equals image after surjection

Stream: Is there code for X?

[Pedro Minicz]

Do we have the following in mathlib? I looked for it but I nor library_search could find it.

import data.set.basic

example {α β γ : Type*} (f : β → α) {g : γ → β} :
  function.surjective g → set.range f = set.range (f ∘ g) :=
begin
  intro hg,
  ext a,
  split; intro h,
  { rcases h with ⟨b, rfl⟩,
    specialize hg b,
    rcases hg with ⟨c, rfl⟩,
    exact ⟨c, rfl⟩ },
  { rcases h with ⟨c, rfl⟩,
    exact ⟨g c, rfl⟩ }
end

[Yaël Dillies]

You can get there faster using docs#set.range_comp