Function to Sum decomposition

Stream: mathlib4

[Martin Dvořák]

Would you add the following into mathlib?

import Mathlib.Tactic

@[simp]
def Function.myEquiv {α β₁ β₂ : Type*} (f : α → β₁ ⊕ β₂) :
    α ≃ { x₁ : α × β₁ // f x₁.fst = Sum.inl x₁.snd } ⊕ { x₂ : α × β₂ // f x₂.fst = Sum.inr x₂.snd } where
  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_myEquiv {α β₁ β₂ : Type*} (f : α → β₁ ⊕ β₂) :
    f = Sum.elim (Sum.inl ∘ (·.val.snd)) (Sum.inr ∘ (·.val.snd)) ∘ myEquiv f := by
  aesop

[Martin Dvořák]

Please review #19323

[Eric Wieser]

This seems rather contrived; can you explain a little more what you need it for, perhaps in the PR description?

[Martin Dvořák]

I find it useful for proving lemmas about TU matrices. I will soon add an example of a proof where I use this construction.

[Eric Wieser]

I think it probably makes sense to make your next PR on top of this one, and only review this on in the context of the application

[Martin Dvořák]

Context (application): #19607