p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
refine' (exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ _
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
have h := Classical.choose_spec (rat_dense' (f i) (div_nat_pos i))
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ (↑i + 1) * ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
refine' lt_of_lt_of_le h ((div_le_iff' <| by exact_mod_cast succ_pos _).mpr _)
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε + 1 * ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ (↑i + 1) * ε
rw [right_distrib]
case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε

case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 ≤ 1 * ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε + 1 * ε
apply le_add_of_le_of_nonneg
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 < ↑i + 1
exact_mod_cast succ_pos _
no goals
case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε
exact (div_le_iff hε).mp (le_trans (le_of_lt hN) (by exact_mod_cast hi))
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ ↑N ≤ ↑i
exact_mod_cast hi
case ha.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 < 1 * ε
case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 ≤ 1 * ε
apply le_of_lt
no goals
case ha.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 < 1 * ε
simpa