@[deprecated map_inj_right_of_nonempty (since := "2025-02-09")]

theorem LawfulFunctor.map_inj_right_of_nonempty {m : Type u_1 → Type u_2} {α β : Type u_1} [Functor m] [LawfulFunctor m] [Nonempty α] {f : α → β} (w : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y

Alias of map_inj_right_of_nonempty.

@[deprecated map_inj_right (since := "2025-02-09")]

theorem LawfulMonad.map_inj_right {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [LawfulMonad m] {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} : f <$> x = f <$> y ↔ x = y

Alias of map_inj_right.