case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑f i) < ε
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
refine' ⟨max N N2, fun i hi ↦ _⟩
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i) + (↑(↑(Padic.lim' f) i) - ↑f i)) < ε
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑f i) < ε
rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i) + (↑(↑(Padic.lim' f) i) - ↑f i)) < ε
refine' (padicNormE.add_le _ _).trans_lt _
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2 + ε / 2
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε
rw [← add_halves ε]
case intro.intro.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) < ε / 2

case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2 + ε / 2
apply _root_.add_lt_add
no goals
case intro.intro.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) < ε / 2
apply hN2 _ (le_of_max_le_right hi)
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (↑f i - ↑(↑(Padic.lim' f) i)) < ε / 2
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2
rw [padicNormE.map_sub]
no goals
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (↑f i - ↑(↑(Padic.lim' f) i)) < ε / 2
exact hN _ (le_of_max_le_left hi)