no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : Generators G → H
⊢ ∃! F, ∀ (a : Generators G), ↑F (of a) = f a
simpa only [Function.funext_iff] using lift.symm.bijective.existsUnique f