## Stream: new members

### Topic: unfold <

#### Chris M (Nov 03 2020 at 16:18):

I have a goal

1 goal
T : Type u_1,
P : T → Prop,
h : FinT T,
h : Π (t : T), decidable (P t),
assum : 0 < sumpred P (count T)
⊢ ∃ (t : T), P t


in the context:

lemma qimpE (T:Type*) (P:T → Prop) [h:FinT T] [h:∀t, decidable (P t)]: nat.zero < (sumpred P (count T))  → ∃t:T, P t :=
begin
intros assum,

end

I want to expand the definition of the < inside assum. dunfold < at assum doesn't work, I presume because < is notation, not a defined term. What is the best way to go about this?


don't unfold!

#### Kenny Lau (Nov 03 2020 at 16:20):

what's your maths proof, and does it involve unfolding <?

#### Chris M (Nov 03 2020 at 16:24):

Well, tbh, my mental definition of a<b is \exists c, a+c=b \and c\neq 0, so that was what I was going for. I have since found out that that is not how it's defined in lean. Under that assumption yes it did involve unfolding <.

#### Chris M (Nov 03 2020 at 16:24):

Kenny Lau said:

don't unfold!

Why do you say this?

#### Kenny Lau (Nov 03 2020 at 16:25):

Because the word "definition" in maths is not the same as in Lean

#### Kenny Lau (Nov 03 2020 at 16:25):

"definition" in Lean should be better translated as "implementation" in maths, since there can only be one definition in Lean, but in maths one thing can have a lot of definitions

#### Kenny Lau (Nov 03 2020 at 16:26):

"definition" in maths would be "definitional lemmas" in Lean, and I can assure you that one exists for this definition you proposed

#### Kenny Lau (Nov 03 2020 at 16:27):

docs#exists_pos_add_of_lt

#### Kenny Lau (Nov 03 2020 at 16:28):

so for example in Lean I might define three to be 3, and then prove that 2 + 1 is an equivalent definition, i.e. prove a lemma saying that three = 2 + 1

#### Kenny Lau (Nov 03 2020 at 16:28):

I will even prove that three = 3 as a separate lemma just to discourage people from ever unfolding three

#### Kenny Lau (Nov 03 2020 at 16:30):

docs#def (this link doesn't work: how do I find all the lemmas containing def?)

#### Chris M (Nov 03 2020 at 17:04):

I see. Thanks :)

By the way I had trouble figuring out how to use exists_pos_add_of_lt. It gives me an error unknown identifier 'exists_pos_add_of_lt'. Clearly I should first open some namespace but I'm not sure how to figure out which one.

#### Mario Carneiro (Nov 03 2020 at 17:07):

I usually type exists_pos_add_of_lt and find the one I want in the ctrl-space dropdown

#### Mario Carneiro (Nov 03 2020 at 17:07):

I would guess it is nat.exists_pos_add_of_lt

#### Kevin Buzzard (Nov 03 2020 at 18:15):

#check exists_pos_add_of_lt ctrl-space says it's in the root namespace (I have import tactic` at the top of my file though)

Last updated: May 10 2021 at 19:16 UTC