Theorem: ULift.surjective_iff_surjective (Jordan/Mathlib/ULift.lean)

State before:
α : Type u
β : Type v
f : α → β
⊢ Iff (Function.Surjective.{max (u_1 + 1) (u + 1), max (u_2 + 1) (v + 1)} (ULift.map.{u, v, u_1, u_2} f))
    (Function.Surjective.{u + 1, v + 1} f)
Tactic:
rw [← Equiv.comp_surjective, comp_uLift_eq_uLift_comp, Equiv.surjective_comp]
State after:
no goals