Exists unique anonymous constructor

Stream: general

[Quinn Culver]

What is the following anonymous constructor doing? It seems somehow to be proving existence & uniqueness at the same time.

lemma has_points.exists_unique_point [has_points P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) :
  ∃! p, p ∈ l₁ ∧ p ∈ l₂ :=
⟨mk_point hl, mk_point_ax hl,
  λ p hp, (eq_or_eq hp.1 (mk_point_ax hl).1 hp.2 (mk_point_ax hl).2).resolve_right hl⟩

That's from line 94 of combinatorics.configuration

[Eric Wieser]

Have you looked at the definition of docs#exists_unique?

[Quinn Culver]

Yeah I have. Is there something there that has the answer?

[Eric Wieser]

⟨mk_point hl, mk_point_ax hl,
  λ p hp, (eq_or_eq hp.1 (mk_point_ax hl).1 hp.2 (mk_point_ax hl).2).resolve_right hl⟩

is short for

⟨mk_point hl,
  ⟨mk_point_ax hl,
    λ p hp, (eq_or_eq hp.1 (mk_point_ax hl).1 hp.2 (mk_point_ax hl).2).resolve_right hl⟩⟩

which is short for

exists.intro (mk_point hl)
  (and.intro (mk_point_ax hl)
    (λ p hp, (eq_or_eq hp.1 (mk_point_ax hl).1 hp.2 (mk_point_ax hl).2).resolve_right hl))

[Eric Wieser]

The exists.intro and and.intro are inferred from the definition at the link I gave

[Patrick Massot]

You can also use

set_option pp.implicit true
#print has_points.exists_unique_point