Never mind

Stream: new members

[Martin Epstein]

I would like to prove this extremely difficult theorem:

example (n : ℕ) (P : ℕ → Prop := fun x => n = x) : P n := by
  sorry

Here is the infoview:

n : ℕ
P : ℕ → Prop
⊢ P n

The definition of P has mysteriously vanished. If I enter unfold P then I get the error "Tactic unfold failed: Local variable P has no definition". Is there a way to finish this proof or have I set it up incorrectly somehow?

[Wang Jingting]

I think the thing you put after := is something like a default value for an argument of the function, but that's not the only value the argument could take.

[Martin Epstein]

I just came up with this solution:

example (n : ℕ) (P : ℕ → Prop)
(P_def : ∀ m, P m ↔ m = n) : P n := by
  specialize P_def n
  rw [P_def]

[Martin Epstein]

Wang Jingting said:

I think the thing you put after := is something like a default value for an argument of the function, but that's not the only value the argument could take.

Interesting, thanks.