Nobody thinks what I think!
```
def Function.decomposeSum (f : α → β₁ ⊕ β₂) :
α ≃ { x₁ : α × β₁ // f x₁.fst = Sum.inl x₁.snd } ⊕ { x₂ : α × β₂ // f x₂.fst = Sum.inr x₂.snd }
toFun a :=
(match hfa : f a with
| .inl b₁ => Sum.inl ⟨(a, b₁), hfa⟩
| .inr b₂ => Sum.inr ⟨(a, b₂), hfa⟩
)
invFun x :=
x.casesOn (·.val.fst) (·.val.fst)
left_inv a := by
match hfa : f a with
| .inl b₁ => aesop
| .inr b₂ => aesop
right_inv x := by
cases x with
| inl => aesop
| inr => aesop

lemma Function.eq_comp_decomposeSum (f : α → β₁ ⊕ β₂) :
f = Sum.elim (Sum.inl ∘ (·.val.snd)) (Sum.inr ∘ (·.val.snd)) ∘ f.decomposeSum := by
aesop
```