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

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