How to prove goals with ∃! (ExistsUnique predicate)

Stream: new members

[D A L]

Problem source: https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_2_2.lean
There was a hint to use one of a few provided APIs, but I am not sure what the correct way to do that is. I attempted the following:

/-
The following API for ∃! may be useful for the next problem.  Also, the `obtain` tactic is useful

for extracting witnesses from existential statements; for instance, `obtain ⟨ x, hx ⟩ := h`

extracts a witness `x` and a proof `hx : P x` of the property from a hypothesis `h : ∃ x, P x`.
-/

#check existsUnique_of_exists_of_unique

#check ExistsUnique.exists

#check ExistsUnique.unique

/-- Lemma 2.2.10 (unique predecessor) / Exercise 2.2.2 -/

lemma Nat.uniq_succ_eq (a:Nat) (ha: a.isPos) : ∃! b, b++ = a := by

  apply existsUnique_of_exists_of_unique

  sorry

But that resulted in an error: "by tac constructs a term of the expected type by running the tactic(s) tac." The online documentation for existsUnique_of_exists_of_unique didn't include any plain English examples of how to use it. In this example problem, what are the Sort and Prop, and why do there need to be new variables y1 and y2? existsUnique_of_exists_of_unique.{u_1} {α : Sort u_1} {p : α → Prop} (hex : ∃ x, p x)

(hunique : ∀ (y₁ y₂ : α), p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x

[Aaron Liu]

Are you sure it's not just unsolved goals?

[Aaron Liu]

apply existsUnique_of_exists_of_unique gives you two new goals.

[D A L]

Aaron Liu said:

apply existsUnique_of_exists_of_unique gives you two new goals.

I assumed that there was some issue, because one of the new goals is a near exact copy of the original goal: case hex
a : Nat
ha : a.isPos
⊢ ∃ x, x++ = a
If applying that theorem doesn't change the goal, then how is it possible to make progress on it?

[Aaron Liu]

That's a different goal, you changed the ExistsUnique to just Exists

[Aaron Liu]

existsUnique_of_exists_of_unique will in fact require you to prove existence (and also uniqueness, separately)

[Aaron Liu]

that's why it gives you two goals, one for existence, and one for uniqueness

[D A L]

Thank you so much, that is the clearest description of that tactic that I was able to find. So, I'm guessing that I would use ExistsUnique.exists and ExistsUnique.unique if I just want to prove existence (former) or just uniqueness (latter) and disregard the other for now?

[Kenny Lau]

D A L said:

Thank you so much, that is the clearest description of that tactic that I was able to find.

It is actually very clear from the name, if you know about Lean's naming convention.

The "of" in a naming convention means B implies A (in the opposite direction), so existsUnique_of_exists_of_unique means that it will prove existsUnique (the first part of the name), provided that you give it a proof of exists (the middle part), and a proof of unique (the last part).

In more symbols, existsUnique_of_exists_of_unique is literally translating the implication:

• Exists → Unique → ExistsUnique

using Lean's naming convention

[Aaron Liu]

D A L said:

Thank you so much, that is the clearest description of that tactic that I was able to find. So, I'm guessing that I would use ExistsUnique.exists and ExistsUnique.unique if I just want to prove existence (former) or just uniqueness (latter) and disregard the other for now?

Unique existence will always require both existence and uniqueness. You can't skip one or the other. The lemmas ExistsUnique.exists and ExistsUnique.unique are actually how you use a statement of unique existence. ExistsUnique.exists let you prove existence from unique existence, and ExistsUnique.unique lets you prove uniqueness.