-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem exists_mem_range : ∃ n : ℕ, n < p ∧ x - n ∈ maximalIdeal ℤ_[p]

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ = ‖↑r - ↑x + ↑x‖

Tactic:
ring_nf

Result:
no goals

Proof state:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ ‖x - ↑n‖ < 1

Tactic:
simp only [norm_def, coe_sub, Subtype.coe_mk, coe_natCast] at hn ⊢

Result:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑n‖ < 1

Proof state:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H

Result:
case intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < ↑p
hn : ‖⟨↑r, H⟩ - ↑n‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Proof state:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑n‖ < 1

Tactic:
rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]

Result:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r + (↑r - ↑n)‖ < 1

Proof state:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r + (↑r - ↑n)‖ < 1

Tactic:
apply lt_of_le_of_lt (padicNormE.nonarchimedean _ _)

Result:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r‖ ⊔ ‖↑r - ↑n‖ < 1

Proof state:
case intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < ↑p
hn : ‖⟨↑r, H⟩ - ↑n‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
lift n to ℕ using hzn

Result:
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ n < p ∧ ‖x - ↑n‖ < 1

Tactic:
constructor

Result:
case h.left
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ n < p

case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ ‖x - ↑n‖ < 1

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ‖↑r‖ ≤ 1

Tactic:
rw [norm_sub_rev] at hr

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ ≤ 1

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one

Result:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃ n < p, x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ ≤ 1

Tactic:
calc
  _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
  _ ≤ _ := padicNormE.nonarchimedean _ _
  _ ≤ _ := max_le (le_of_lt hr) x.2

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ↑x - ↑n = ↑x - ↑r + (↑r - ↑n)

Tactic:
ring

Result:
no goals

Proof state:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1

Tactic:
simpa using hn

Result:
no goals

Proof state:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r‖ ⊔ ‖↑r - ↑n‖ < 1

Tactic:
apply max_lt hr

Result:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1

Proof state:
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
use n

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ n < p ∧ ‖x - ↑n‖ < 1

Proof state:
case h.left
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ n < p

Tactic:
exact mod_cast hnp

Result:
no goals

Proof state:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
have H : ‖(r : ℚ_[p])‖ ≤ 1 := by
  rw [norm_sub_rev] at hr
  calc
    _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
    _ ≤ _ := padicNormE.nonarchimedean _ _
    _ ≤ _ := max_le (le_of_lt hr) x.2

Result:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1