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

@[simp]

theorem 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

@[simp]

theorem 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