## Stream: new members

### Topic: subtype question

#### Anca Ciobanu (May 31 2019 at 11:44):

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
(H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y := sorry


How do you prove this? I tried induction H and I seemed to lose my hypothesis.

#### Kevin Buzzard (May 31 2019 at 11:46):

ha ha! Induction H seems to leave you in an unprovable state! What's going on there?

#### Kevin Buzzard (May 31 2019 at 11:47):

ha ha, revert H, simp works :D

#### Kevin Buzzard (May 31 2019 at 11:47):

This should be trivial

#### Kevin Buzzard (May 31 2019 at 11:50):

I am totally confused

#### Kevin Buzzard (May 31 2019 at 11:51):

set_option trace.simplify.rewrite true
example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
(H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y :=
begin
revert H,
simp,
/-
0. [simplify.rewrite] [imp_self]: x = y → x = y ==> true
-/
end


#### Kevin Buzzard (May 31 2019 at 11:51):

simp won't tell me how it did it!

#### Chris Hughes (May 31 2019 at 11:52):

It uses subtype.mk.inj_eq

I think

#### Kevin Buzzard (May 31 2019 at 11:55):

? This says <x,hx>=<y,hy> = (x = y) so now I have to jump through some hoops to make this. Anca is in tehe middle of a tactic proof and has H : <x,hx>=<y,hy> and we just want x=y.

#### Mario Carneiro (May 31 2019 at 11:58):

cases

#### Kevin Buzzard (May 31 2019 at 11:59):

cases H doesn't work!

you sure?

#### Kevin Buzzard (May 31 2019 at 11:59):

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
(H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y :=
begin
cases H,
/-
cases tactic failed, unexpected failure when introducing auxiliary equatilies
-/

end


#### Kevin Buzzard (May 31 2019 at 11:59):

What is an equatily?

#### Mario Carneiro (May 31 2019 at 11:59):

woah that's a new one

#### Mario Carneiro (May 31 2019 at 12:00):

I think you found the bug

#### Mario Carneiro (May 31 2019 at 12:01):

injection should work

#### Mario Carneiro (May 31 2019 at 12:04):

the term proof is subtype.no_confusion H id or subtype.mk.inj H

#### Mario Carneiro (May 31 2019 at 12:07):

you can also simp at H

#### Xindi Ai (May 31 2019 at 13:59):

(I am new to Lean so please excuse my style)
I ran into a similar problem before and what I roughly did was

def mysubtype (X : Type) (P : X → Prop) : Type := {x : X // P x}

def myfun (X : Type) (P : X → Prop): mysubtype X P → X
|⟨x, hx⟩ := x

lemma mylemma (X : Type) (P : X → Prop) (x : X) (hx : P x): myfun X P ⟨x, hx⟩ = x := rfl

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
(H : (⟨x, hx⟩ : mysubtype X P) = ⟨y, hy⟩ ) : x = y :=
congr_arg (myfun X P) H


Seems to be a bit of a detour though.

#### Kevin Buzzard (May 31 2019 at 14:02):

Seems to be a bit of a detour though.

Yes! That was the annoying thing. I was showing an undergraduate how to use Lean and then this came up, and all of a sudden the whole thing looked far more complicated than it should have been.

#### Floris van Doorn (May 31 2019 at 19:10):

injection H is probably the best way to so this. Another possibility is congr_arg subtype.val H

#### Jesse Michael Han (May 31 2019 at 19:16):

laziest solution:

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
(H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y :=
begin
library_search
-- exact subtype.mk.inj H
end


Last updated: May 07 2021 at 00:30 UTC