A basic equivalence

Stream: Is there code for X?

[Xavier Roblot]

I need the following

import Mathlib.Logic.Equiv.Defs

variable {α β : Type*} (p : α → Prop)

example : {s : α × β // p s.1} ≃ {a // p a} × β where
  toFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩
  invFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

The proof is so simple that I thought I could construct it from the results in Mathlib.Logic.Equiv.Basic, but I couldn't find a simple way of doing it. Am I missing something? Is it worth adding?

[Markus Himmel]

This is quite close to docs#Equiv.subtypeProdEquivProd and docs#Equiv.subtypeProdEquivSigmaSubtype but I don't think it follows trivially from either, so I think it would be good to add it.

[Xavier Roblot]

Yeah, I tried to use these two equivalences to get the result I wanted but I could not make it work.

[Xavier Roblot]

This one docs#Equiv.subtypeSigmaEquiv is also very close.

[Xavier Roblot]

#12802