Commit 2022-12-15 19:18 1305c799
View on Github →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.