p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∃ n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]
simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
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
case intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑n‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
case intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑n‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
lift n to ℕ using hzn
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ n < p ∧ ‖x - ↑n‖ < 1
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ ∃ n, n < p ∧ ‖x - ↑n‖ < 1
use n
case intro.intro.intro.intro.intro.left
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ n < p

case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ ‖x - ↑n‖ < 1
case intro.intro.intro.intro.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ n < p ∧ ‖x - ↑n‖ < 1
constructor
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑n‖ < 1
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ ‖x - ↑n‖ < 1
simp only [norm_def, coe_sub, Subtype.coe_mk, coe_nat_cast] at hn⊢
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r + (↑r - ↑n)‖ < 1
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑n‖ < 1
rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ max ‖↑x - ↑r‖ ‖↑r - ↑n‖ < 1
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑x - ↑r + (↑r - ↑n)‖ < 1
apply lt_of_le_of_lt (padicNormE.nonarchimedean _ _)
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ max ‖↑x - ↑r‖ ‖↑r - ↑n‖ < 1
apply max_lt hr
no goals
case intro.intro.intro.intro.intro.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1
simpa using hn
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ ≤ 1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
⊢ ‖↑r‖ ≤ 1
rw [norm_sub_rev] at hr
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ ≤ 1
calc
  _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
  _ ≤ _ := padicNormE.nonarchimedean _ _
  _ ≤ _ := max_le (le_of_lt hr) x.2
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ = ‖↑r - ↑x + ↑x‖
ring_nf
no goals
case intro.intro.intro.intro.intro.left
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖{ val := ↑r, property := H } - ↑↑n‖ < 1
⊢ n < p
exact_mod_cast hnp
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r✝ : ℚ
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ↑x - ↑n = ↑x - ↑r + (↑r - ↑n)
ring