A question about getting a map

Stream: maths

[Junqi Liu]

If I have such lemma

lemma P {f : ℕ → ℝ} (r : ℕ) : ∃ a : ℤ, r = a / f r := by sorry

How can I get a map which maps $r$ to $a$ in lemma P?

[Kevin Buzzard]

In tactic mode you can use the choose tactic and in term mode you can use (P r).choose for the function and (P r).choose_spec for the equality defining the function.

[Junqi Liu]

oh! Cool! I have solved my sorry by your suggestion! Thanks a lot!