-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem complete' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (q - f i : ℚ_[p]) < ε :=
  ⟨lim f, fun ε hε ↦ by
    obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)
    obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)
    refine ⟨max N N2, fun i hi ↦ ?_⟩
    rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]
    refine (padicNormE.add_le _ _).trans_lt ?_
    rw [← add_halves ε]
    apply _root_.add_lt_add
    · apply hN2 _ (le_of_max_le_right hi)
    · rw [padicNormE.map_sub]
      exact hN _ (le_of_max_le_left hi)⟩

Proof state:
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2

Tactic:
rw [padicNormE.map_sub]

Result:
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (↑f i - ↑(↑(Padic.lim' f) i)) < ε / 2

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε

Tactic:
obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε

Tactic:
obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i) + (↑(↑(Padic.lim' f) i) - ↑f i)) < ε

Tactic:
refine (padicNormE.add_le _ _).trans_lt ?_

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2 + ε / 2

Tactic:
apply _root_.add_lt_add

Result:
case intro.intro.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ 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 ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2

Proof state:
case intro.intro.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) < ε / 2

Tactic:
apply hN2 _ (le_of_max_le_right hi)

Result:
no goals

Proof state:
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (↑f i - ↑(↑(Padic.lim' f) i)) < ε / 2

Tactic:
exact hN _ (le_of_max_le_left hi)

Result:
no goals

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε

Tactic:
rw [← add_halves ε]

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2 + ε / 2

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑f i) < ε

Tactic:
rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i) + (↑(↑(Padic.lim' f) i) - ↑f i)) < ε

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε

Tactic:
refine ⟨max N N2, fun i hi ↦ ?_⟩

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ N ⊔ N2
⊢ padicNormE (Padic.lim f - ↑f i) < ε