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

theorem map_inj_of_inj {m : Type u_1 → Type u_2} {α β : Type u_1} [Applicative m] [LawfulApplicative m] [Nonempty α] {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) {x y : m α} (h : f <$> x = f <$> y) : x = y