Convert from a decidable Subtype equivalence to a PEquiv

Stream: Is there code for X?

[Dylan Ede]

I.e. is there an existing function to, given DecidablePred p, {x : α // p x} ≃ β, get a α ≃. β?

[Dylan Ede]

In case anyone else is interested, I came up with this implementation. Bear in mind I'm new to Lean so the proof might not be the nicest (a review would be welcome).

def Equiv.subtypeToPEquiv {p : β -> Prop} [DecidablePred p] (eqv : α ≃ {x : β // p x}) : α ≃. β where
  toFun := some ∘ Subtype.val ∘ eqv
  invFun := fun x => if h : p x then eqv.symm ⟨x, h⟩ else none
  inv := by
    intros a b
    simp
    by_cases h : p b
    . simp [h]
      apply Iff.intro
      . intro h'
        rw [<-eqv.symm_apply_eq.mp h']
      . intro h'
        rw [eqv.symm_apply_eq, Subtype.coe_eq_of_eq_mk h']
    . simp [h]
      contrapose! h
      have := (eqv a).prop
      rwa [h] at this

[Dylan Ede]

I've just noticed this depends on Classical.choice, which is not ideal.

[Dylan Ede]

And it's due to the use of by_cases and contrapose!. I've replaced the use of by_cases with cases Decidable.em (p b), just trying to figure out how to not use contrapose! now.

[Yaël Dillies]

Dylan Ede said:

I.e. is there an existing function to, given DecidablePred p, {x : α // p x} ≃ β, get a α ≃. β?

Seems like it doesn't exist

[Dylan Ede]

Now I have

def Equiv.subtypeToPEquiv {p : β -> Prop} [DecidablePred p] (eqv : α ≃ {x : β // p x}) : α ≃. β where
  toFun := some ∘ Subtype.val ∘ eqv
  invFun := fun x => if h : p x then eqv.symm ⟨x, h⟩ else none
  inv := by
    intros a b
    simp
    cases Decidable.em (p b)
    case inl h =>
      simp [h]
      apply Iff.intro
      case mp =>
        intro h'
        rw [<-eqv.symm_apply_eq.mp h']
      case mpr =>
        intro h'
        rw [eqv.symm_apply_eq, Subtype.coe_eq_of_eq_mk h']
    case inr h =>
      simp [h]
      intro h'
      apply h
      have := eqv a |>.prop
      rwa [h'] at this

which is now purely constructive.

[Dylan Ede]

Realised that by_cases is not actually using classical logic (must be using the Decidable instance and being cleverer than I thought). Now I have

def Equiv.subtypeToPEquiv {p : β -> Prop} [DecidablePred p] (eqv : α ≃ {x : β // p x}) : α ≃. β where
  toFun := some ∘ Subtype.val ∘ eqv
  invFun := fun x => if h : p x then eqv.symm ⟨x, h⟩ else none
  inv := by
    intros a b
    simp
    by_cases p b
    case pos h =>
      simp [h]
      refine ⟨fun h' => ?mp, fun h' => ?mpr⟩
      case mp => rw [<-eqv.symm_apply_eq.mp h']
      case mpr => rw [eqv.symm_apply_eq, Subtype.coe_eq_of_eq_mk h']
    case neg h =>
      simp [h]
      intro h'
      apply h
      subst h'
      exact eqv a |>.prop