no goals
α : Type u_1
β : Type ?u.5932
γ : Type ?u.5935
ι : Sort u_2
π : α → Type ?u.5943
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Injective (codRestrict f s h) ↔ Injective f
simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]