simp_rw [image_image, coe_inclusion]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
r : Set ↑s
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => inclusion ht (f x)) '' r) = ↑(f '' r)
no goals