Subtypes and equality

Stream: lean4

[Evante Garza]

I'm getting stuck on trying to show this example:

example {X : Sort _} {P Q : X -> Prop} (h : Subtype P = Subtype Q) : ∀ x : X, P x <-> Q x

the other direction was fairly straightforward, but for this example I can't figure out how to use h.

  intro x
  apply Iff.intro
  . intro mp -- P x
    let xq : Subtype Q := h ▸ ⟨x, mp⟩
    have : xq.val = x := by rfl

If I try this, rfl fails. I run into a similar problem with rewriting:

  . intro mp
    let xp : Subtype P := ⟨x, mp⟩
    rw [h] at xp
    have : xp.val = x := by rfl

Again rfl fails, but will succeed if the rewrite is commented out.

The actual problem I'm trying to solve could be done with subsets instead of subtypes, but I'm interested in seeing how far I can go without making that change.

[Kevin Buzzard]

Equality of types is "evil" in Lean -- for example Nat = Int is undecidable and your example might be too. In the cardinality model of Lean's type theory the subtypes might be equal simply because they have the same size.