Extracting quantifier data

Stream: new members

[THEODORE GONZALES]

Hello! I am a new user and I am trying to understand how to obtain data from propositions like the following:

def is_polynomial (f: ℤ → ℂ) : Prop :=
∃ z : ℤ, (z > 0 ) ∧ (∀ j : ℤ, z ≤ |j| → f j = 0)

I want to be able to define a function which uses the z given by an assumption hf : is_polynomial f for some f: Z -> C but I am not sure how to obtain the z given by the proposition hf : is_polynomial f. Is there an easy way to obtain the values given by an existential quantifier from a proposition?

Thank you!

[Ruben Van de Velde]

Can you write a #mwe of what you're trying to do?

[Alex J. Best]

docs#classical.some is the standard way to "extract" data from an existential, using choice.
You can then use docs#classical.some_spec to have a proof that the extracted value satisfies the inner part of the existential

[Riccardo Brasca]

You can also use the tactic obtain

[THEODORE GONZALES]

import data.real.basic
import data.complex.basic

def is_polynomial (f: ℤ → ℂ) : Prop :=
∃ z : ℤ, (z > 0 ) ∧ (∀ j : ℤ, z ≤ |j| → f j = 0)

def fin_sup_poly := λ (f: ℤ → ℂ) (hf : is_polynomial f),
"here I want to use the value z given by hf"

[THEODORE GONZALES]

Ah okay I will have to read up on these tactics. Thank you.

[Patrick Massot]

You should also read #backticks

[THEODORE GONZALES]

Ah okay will do thank you.

[Patrick Massot]

No problem, everybody needs to go through those stages of learning!

[Junyan Xu]

Is https://leanprover-community.github.io/mathlib_docs/tactic/expand_exists.html now the recommended way to do such things?
By the way, docs#laurent_polynomial and docs#finsupp already exists.

[THEODORE GONZALES]

Ah I figured someone had already done this. Do y'all know if anyone has done Vertex Operator Algebras quite yet ?

[Kevin Buzzard]

I think vertex operator algebras are still not there but you'll have to wait for someone else to tell you how far away they are.

[THEODORE GONZALES]

I am currently taking a course on VOA's and was hoping to formalize props in it in lean while in the course, but I guess I should probably know how to use lean first lol

[Kevin Buzzard]

To be honest a great way to learn Lean is to actually try to do stuff in Lean and ask here if you get stuck (although you might want to start a new topic, right now we're apparently still talking about extracting quantifier data).

[THEODORE GONZALES]

Yeah ill just try to do whatever I can and hopefully that will teach me how to use lean haha

[Kevin Buzzard]

that's what I said 5 years ago