# Zulip Chat Archive

## 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`

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

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!

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

This is why we asked.

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

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