Commit 2022-12-15 19:18 1305c799

fix: alias uses type of lemma (#1058) #check @Function.Surjective.range_eq now gives

@Surjective.range_eq : ∀ {α : Type u_2} {ι : Sort u_1} {f : ι → α}, Surjective f → range f = univ

as expected.