no goals
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ (x : ι), x ∈ univ → ∀ (y : ι), y ∈ univ → f x = f y → x = y) ↔ Function.Injective f
simp_rw [mem_univ, true_imp_iff, Function.Injective]