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

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