rw [← image_univ, image_val_image_comp_inclusion]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑(range fun x => inclusion ht (f x)) = ↑(range f)
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => f x) '' univ) = ↑(range f)