Replace definition of Exists with the actual one from core.lean

[peterzeller]

Did not understand the definition in the tutorial, so looked up the actual definition.

[Kha]

This is not consistent with the style of other inductive declarations in this chapter, e.g. Sigma above and Subtype below. Please give a better motivation for this change, what makes the new definition easier to understand in your eyes?

[peterzeller]

Ok, found out why I read it wrong. Feel free to close this PR.

I thought precedence was like this:

inductive Exists {α : Type u} (q : α → Prop) : Prop where
  | intro : (∀ (a : α), q a) → Exists q

But it is like this:

inductive Exists {α : Type u} (q : α → Prop) : Prop where
  | intro : ∀ (a : α), (q a → Exists q)

I guess I read it that way because the pattern at the beginning was:

    inductive Foo where
      | constructor₁ : ... → Foo
      | constructor₂ : ... → Foo
      ...
      | constructorₙ : ... → Foo

So I matched the ... against the left part of the arrow.

I understand that the two are equivalent now, but I think the one without ∀ is still clearer as I can directly see that Exists.intro takes two arguments, which I already know from the previous section.

And Sigma and Subtype are also defined without ∀ in the tutorial.

[Kha]

Okay, that's fair. It looks like ∀ is first used in chapter 3, but not actually introduced before that. That could definitely be improved.