case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
⊢ ∃ q, ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - q) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
⊢ ∃ q, ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - q) < ε
obtain ⟨x, hx⟩ := complete' f
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - x) < ε
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
⊢ ∃ q, ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - q) < ε
refine ⟨x, fun ε hε => ?_⟩
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - x) < ε
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - x) < ε
obtain ⟨N, hN⟩ := hx ε hε
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (↑f i - x) < ε
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - x) < ε
refine ⟨N, fun i hi => ?_⟩
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (x - ↑f i) < ε
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (↑f i - x) < ε
rw [padicNormE.map_sub]
no goals
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (x - ↑f i) < ε
exact hN i hi