Stuck at proof about p-adic numbers (epsilon condition)

Stream: general

[Mario Weitzer]

How do I prove the following? (in Lean 3)

import number_theory.padics.padic_numbers

variables {p : ℕ} [fact p.prime]

example (d : ℚ_[p]) (ε : ℚ) (hε : 0 < ε) :
  ∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → padic_norm_e ((quotient.out d j) - d) < ε :=
begin
  sorry
end

[Ruben Van de Velde]

What's the proof?

[Mario Weitzer]

Isn‘t this true by definition? The p-adic number d is the limit of every sequence in the class of Cauchy sequences that represent it, one of which is picked by quotient.out. And convergence is defined in terms of the p-adic norm.

[Kevin Buzzard]

Mathematicians are great at claiming that a whole bunch of things are true "by definition" :-)

[Kevin Buzzard]

Can you make your question into a #mwe Mario? Add any import and open etc in order to make the code block compile just by cutting and pasting; this makes it much easier for others to experiment with your question.

[Kevin Buzzard]

docs#padic_norm_e

[Mario Weitzer]

Ah sorry, I included the stuff about p being prime but forgot about the import. I edited the example and it should compile now.

Yes, I meant it should be true by definition to a mathematician but to be fair, I was asked for a mathematician‘s proof (at least that‘s how I understood the question) ;).

[Patrick Massot]

This is essentially the very next declaration in the same file docs#padic_norm_e.defn

[Patrick Massot]

import number_theory.padics.padic_numbers

variables {p : ℕ} [fact p.prime]

example (d : ℚ_[p]) (ε : ℚ) (hε : 0 < ε) :
  ∃ (i : ℕ), ∀ (j : ℕ), j ≥ i → padic_norm_e ((quotient.out d j) - d) < ε :=
by  simpa only [padic_norm_e.map_sub, quotient.out_eq d] using padic_norm_e.defn (quotient.out d) hε

[Mario Weitzer]

Perfect, thank you!