case intro
α : Type u_2
β : Type u_1
γ : Type ?u.34812
ι : Sort ?u.34815
π : α → Type ?u.34820
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i => f ↑i
⊢ ∃ f, InjOn f s
α : Type u_2
β : Type u_1
γ : Type ?u.34812
ι : Sort ?u.34815
π : α → Type ?u.34820
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : ↑s → β
hf : Injective f
⊢ ∃ f, InjOn f s
lift f to α → β using trivial
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.34812
ι : Sort ?u.34815
π : α → Type ?u.34820
s s₁ s₂ : Set α
t t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
inst✝ : Nonempty β
x✝ : ∃ f, Injective f
f : α → β
hf : Injective fun i => f ↑i
⊢ ∃ f, InjOn f s
exact ⟨f, injOn_iff_injective.2 hf⟩