Are elements of a subtype determined by their value?

Stream: general

[Johan Commelin]

import order.bounds algebra.ordered_group analysis.real analysis.topology.infinite_sum
noncomputable theory

definition nnreal := {r : ℝ // 0 ≤ r}
notation ` ℝ≥0 ` := nnreal

lemma val_eq_val (r₁ r₂ : ℝ≥0) : r₁ = r₂ ↔ r₁.val = r₂.val := sorry

I want to mutter something about proof-irrelevance... and of course I'm working classical

[Kenny Lau]

yes. subtype.eq

[Johan Commelin]

Ok, thanks!

[Johan Commelin]

That is helpful

[Johan Commelin]

I expected that to be right after the definition of a subtype, but I should have thought of looking for a separate file

[Kenny Lau]

mathlib vs core :)

[Johan Commelin]

I see

[Kevin Buzzard]

All methods have advantages and disadvantages but the reason I'm mentioning this is that it's important to get into the right mindset.

[Kevin Buzzard]

The logic is "it's important, so it's probably there already, so I could either plough through subtype.lean, or guess what the theorem might be called and try and find it with the ctrl-space dance, or just ask here"

[Kevin Buzzard]

my posts are appearing in random orders

[Kevin Buzzard]

I asked here too much in the early days and it took me a while to figure out the other algorithms, it's a sort of "give a man a fish" thing, and of course asking here is a super-helpful resource, but somehow I understand the other possibilities better now and once you understand them you become more powerful.

[Kevin Buzzard]

And of course from where you're sitting you have no idea about what will be in core and what will be in mathlib, so sometimes it's just less frustrating to ask

[Kevin Buzzard]

What it took me a long time to understand was "if it's natural, it's already there, and is almost certainly named well"

[Johan Commelin]

Ok, so I applied your strategy, and expected there to be a subtype.neq. But it's not there...

[Kenny Lau]

someone is being too classical

[Kenny Lau]

it's just a rw for the other direction

[Kevin Buzzard]

You should add it :-)

[Kevin Buzzard]

subtype.eq is an iff

[Johan Commelin]

Hmm, so I should rw, instead of apply...?

[Mario Carneiro]

There aren't a lot of negated theorems like that, since mt is literally two characters and turns any A -> B into \not B -> \not A

[Kenny Lau]

congr_arg subtype.val, whatever

[Kevin Buzzard]

If H is A <-> B then H.1 is A -> B and H.2 is B -> A, if this helps

[Kevin Buzzard]

(this is because the _definition_ of <-> is what you think it is)

[Johan Commelin]

Wait, how do I use mt?

[Kevin Buzzard]

#print mt

[Johan Commelin]

Hmmz, I see

[Kevin Buzzard]

or #check mt if you just want to see the type

[Kevin Buzzard]

Some questions of the form "how do I use X" are really "what is its type?" and some are "what is its definition?"

[Johan Commelin]

Stuff isn't typechecking over here... I'll have to work a bit

[Kevin Buzzard]

so you use #check or #print

[Kevin Buzzard]

That's another thing I learnt -- when I get errors now I read them carefully

[Kevin Buzzard]

because they tell you exactly what you have got wrong

[Johan Commelin]

Ok, so my subtype.eq is not an iff, it's something from core saying

protected lemma eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl

[Kevin Buzzard]

OK great -- I just assumed it was an iff from something someone said earlier

[Kevin Buzzard]

I guess it's protected because if you open subtype then all of a sudden you have clobbered the definition of eq