Confused with double "exists"

Stream: new members

[Walter Moreira]

I'm going over the tutorial proposed by @Patrick Massot . I'm confused about what it means the double "exists" in a judgement like

key : ∀ (n : ℕ), ∃ (a : ℝ) (H : a ∈ A), a < x + 1 / (↑n + 1)

How does that notation translates into bare Exists? Is it a way to ask Lean to display the unfolding of the definition?

[Reid Barton]

It means

key : ∀ (n : ℕ), ∃ (a : ℝ), ∃ (H : a ∈ A), a < x + 1 / (↑n + 1)

[Walter Moreira]

Thank you @Reid Barton That's what I was expecting. I got confused about it with the application of choose u hu using key which added

hu : ∀ (n : ℕ), u n ∈ A ∧ u n < x + 1 / (↑n + 1)

and I couldn't see how Lean was generating the $\wedge$ in that clause. It seems that it becomes more clear when doing choose u v hu which generates two functions.

I guess that Lean automatically combines them with $\wedge$ if I provide only one variable?

[Reid Barton]

I think the choose tactic has some specific magic to get rid of unnecessary ∃ (in the sense that the variable, here H, is not used) and turn them into ∧.

[Patrick Massot]

This is very similar to what is explained at https://github.com/leanprover-community/tutorials/blob/a1b5620e098deb0c06c902b1151b02aca5f46033/src/exercises/06_sub_sequences.lean#L67-L73 but I should probably repeat that comment. Also, you can ask Lean to rewrite this abbreviation using rw exists_prop.