# Zulip Chat Archive

## Stream: general

### Topic: calculations with eq

#### Reid Barton (Jun 22 2018 at 17:31):

Is this provable?

lemma eq_mpr_val {α : Type} {p q : α → Prop} (e : subtype p = subtype q) (x : subtype q) : (eq.mpr e x).val = x.val := sorry

#### Reid Barton (Jun 22 2018 at 17:32):

(`subtype`

here is just an example of a type which has a field whose type doesn't depend on the type indices being changed by `e`

.)

#### Reid Barton (Jun 22 2018 at 17:34):

Or if I find myself needing to prove this sort of thing, do I need to back up and make sure that instead of this `eq.mpr e x`

, I have an expression that recurses on a proof of `p = q`

?

#### Simon Hudon (Jun 22 2018 at 17:44):

Yeah, I don't see an alternative. `eq.mpr`

is going to be difficult to get rid of. I tried various things with generalize and congr but to no avail

#### Chris Hughes (Jun 22 2018 at 21:00):

I think it's probably not provable. I don't see a reason why `@subtype.val α p == @subtype.val α q`

without `p = q`

. I think in lean two types of the same size are indistinguishable, so if `p ≠ q`

, but `subtype p = subtype q`

, there's no contradiction, provided they're the same size, but there's no canonical isomorphism or way of identifying `@subtype.val α p`

with `@subtype.val α q`

. Mario will know.

#### Chris Hughes (Jun 22 2018 at 21:03):

I couldn't actually prove a contradiction from assuming `subtype p = subtype q`

, where `p ≠ q`

and your lemma though.

#### Mario Carneiro (Jun 23 2018 at 02:46):

These sorts of things are independent in lean. Injectivity of inductive type constructors is either independent or false in every case I'm aware of.

Last updated: May 13 2021 at 00:41 UTC