no goals
α : Type u_1
β : Type u_2
γ : Type ?u.34549
ι : Sort ?u.34552
π : α → Type ?u.34557
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s
rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]