exists_unique

Stream: new members

[Jiekai]

def P (n : nat) := 3 ≤ n ∧ n < 5

example : ∃! m, P m :=
begin
  split,
  /-
  2 goals
  ⊢ (λ (m : ℕ), P m) ?m_1 ∧ ∀ (y : ℕ), (λ (m : ℕ), P m) y → y = ?m_1

  ⊢ ℕ
  -/

  {
    split,
    {
    /-
    ⊢ (λ (m : ℕ), P m) ?m_1
    -/

    },
    {}
  },
  exact 1,
end

Why are two splits needed?

[Eric Wieser]

Because src#exists_unique is defined as an exists with an and inside it, and each split goes one level at a time

[Eric Wieser]

The usual way to split it would be refine ⟨1, _, _⟩

[Jiekai]

def exists_unique {α : Sort u} (p : α → Prop) :=
∃ x, p x  ∧  ∀ y, p y → y = x
          ↑ the and

The first split seems not spliting this ∧.

[Hanting Zhang]

Your statement needs 3 pieces of information, first a witness x, second a proof that p x is true, and finally a proof that x is unique. You can provide this to lean by giving it a list of (x, p x, unique x). When you use split,