-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem defn (f : PadicSeq p) {ε : ℚ} (hε : 0 < ε) :
    ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - f i : ℚ_[p]) < ε

Proof state:
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ False

Tactic:
apply not_le_of_gt _ hge

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))

Proof state:
case h.h.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
N✝ i✝ : ℕ
a✝ : i✝ ≥ N✝
N : (f - const (padicNorm p) (↑f i✝)).norm < ε
⊢ Quotient.lift PadicSeq.norm ⋯ (Padic.mk f - ↑(↑f i✝)) < ε

Tactic:
use N

Result:
no goals

Proof state:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
hngen : stationaryPoint hne ≤ N
this :
  padicNorm p (↑(f - const (padicNorm p) (↑f i)) N) =
    padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))

Tactic:
rw [← this]

Result:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
hngen : stationaryPoint hne ≤ N
this :
  padicNorm p (↑(f - const (padicNorm p) (↑f i)) N) =
    padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) N)

Proof state:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
hngen : stationaryPoint hne ≤ N
this :
  padicNorm p (↑(f - const (padicNorm p) (↑f i)) N) =
    padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) N)

Tactic:
exact hN _ le_rfl _ hi

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
⊢ ∃ N, ∀ i ≥ N, Quotient.lift PadicSeq.norm ⋯ (Padic.mk f - ↑(↑f i)) < ε

Tactic:
peel hyp with N

Result:
case h.h.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε
N✝ i✝ : ℕ
a✝ : i✝ ≥ N✝
N : (f - const (padicNorm p) (↑f i✝)).norm < ε
⊢ Quotient.lift PadicSeq.norm ⋯ (Padic.mk f - ↑(↑f i✝)) < ε

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Tactic:
rw [PadicSeq.norm, dif_pos h] at hge

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ 0
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
⊢ False

Tactic:
rcases h N with ⟨i, hi, hge⟩

Result:
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ 0
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Tactic:
exact not_lt_of_ge hge hε

Result:
no goals

Proof state:
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) (↑f i)).norm
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Tactic:
unfold PadicSeq.norm at hge

Result:
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge :
  ε ≤
    if hf : f - const (padicNorm p) (↑f i) ≈ 0 then 0
    else padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hf))
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False

Proof state:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
hgen : N ≤ stationaryPoint hne
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))

Tactic:
exact hN _ hgen _ hi

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, (f - const (padicNorm p) (↑f i)).norm < ε

Tactic:
by_contra! h

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
⊢ False

Tactic:
obtain ⟨N, hN⟩ := cauchy₂ f hε

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) (↑f i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p (↑f j - ↑f k) < ε
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - ↑(↑f i)) < ε

Tactic:
dsimp [padicNormE]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ i ≥ N, Quotient.lift PadicSeq.norm ⋯ (Padic.mk f - ↑(↑f i)) < ε