exact ⟨u, hru, hus, h.image_eq, h.injOn⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f : α → β
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
no goals