injection of range of a composition

Stream: Is there code for X?

[Nir Paz]

Do we have this?

import Mathlib

example {α β γ} (f : α → β) (g : β → γ) : Nonempty (Set.range (g ∘ f) ↪ Set.range f) := sorry

[Eric Wieser]

This works:

example {α β γ} (f : α → β) (g : β → γ) : Nonempty (Set.range (g ∘ f) ↪ Set.range f) := by
  rw [← Cardinal.lift_mk_le, Set.range_comp]
  exact Cardinal.mk_image_le_lift.trans_eq <| congr_fun Cardinal.lift_umax'.symm _

[Nir Paz]

Thanks!