p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N,
    ∀ (i : ℕ),
      i ≥ N →
        Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
            (Padic.mk f - ↑(↑f i)) <
          ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.mk f - ↑(↑f i)) < ε
dsimp [padicNormE]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → PadicSeq.norm (f - const (padicNorm p) (↑f i)) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N,
    ∀ (i : ℕ),
      i ≥ N →
        Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
            (Padic.mk f - ↑(↑f i)) <
          ε
change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ False
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → PadicSeq.norm (f - const (padicNorm p) (↑f i)) < ε
by_contra' h
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
⊢ False
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ False
cases' cauchy₂ f hε with N hN
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ False
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
⊢ False
rcases h N with ⟨i, hi, hge⟩
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ False
have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := by
  intro h
  unfold PadicSeq.norm at hge; split_ifs at hge
  exact not_lt_of_ge hge hε
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), 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
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
unfold PadicSeq.norm at hge
case intro.intro.intro.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
h✝ : f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ 0
⊢ False

case intro.intro.intro.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
⊢ False
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), 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
split_ifs at hge
case intro.intro.intro.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
⊢ False
case intro.intro.intro.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
h✝ : f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ 0
⊢ False

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

case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
cases' _root_.em (N ≤ stationaryPoint hne) with hgen hngen
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ ¬f - const (padicNorm p) (↑f i) ≈ 0
intro h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), 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))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
unfold PadicSeq.norm at hge
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
h : f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ 0
⊢ False
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), 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))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
split_ifs at hge
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
h : f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ 0
⊢ False
exact not_lt_of_ge hge hε
no goals
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hgen : N ≤ stationaryPoint hne
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
apply hN _ hgen _ hi
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
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 h✝))
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
have := stationaryPoint_spec hne le_rfl (le_of_not_le hngen)
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
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)
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
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 h✝))
rw [← this]
no goals
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
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)
exact hN _ le_rfl _ hi