Lemmas for maps on finsets

Stream: Is there code for X?

[Michael Stoll]

I have found myself needing the following two results, which I was unable to find in mathlib:

namespace finset

lemma exists_right_inv_on_image {α β} [inhabited α] [decidable_eq β] (f : α → β) (I : finset α) :
  ∃ g : β → α, (∀ b ∈ I.image f, f (g b) = b) ∧ ∀ a ∈ I, g (f a) ∈ I := ...

lemma eq_bUnion_of_fibers {α β} [decidable_eq α] [decidable_eq β] (f : α → β) (I : finset α) :
  I = (I.image f).bUnion (λ m, I.filter (λ j, f j = m)) := ...

They seem natural enough to expect them to be available, though (and their set versions as well).
docs#finset.set_bUnion_preimage_singleton and docs#set.bUnion_preimage_singleton are related to the second one, but different.
Am I overlooking something?

[Yakov Pechersky]

iirc, there's a version of docs#function.inv_fun for fintypes

[Michael Stoll]

Maybe one can use docs#function.inv_fun to simplify the proof I have. Thanks for the pointer!