p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
      (Completion.mk q' - ↑(↑q' N)) <
    ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ ↑padicNormE (Quotient.mk equiv q' - ↑(↑q' N)) < ε
dsimp [padicNormE]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
      (Completion.mk q' - ↑(↑q' N)) <
    ε
convert_to PadicSeq.norm (q' - const _ (q' N) : PadicSeq p) < ε
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
heq : q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε

case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
cases' Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq hne'
no goals
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
heq : q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
simpa only [heq, PadicSeq.norm, dif_pos]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) < ε
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
simp only [PadicSeq.norm, dif_neg hne']
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) < ε
change padicNorm p (q' _ - q' _) < ε
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε

case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : ¬stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
cases' Decidable.em (stationaryPoint hne' ≤ N) with hle hle
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this :
  padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) =
    padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) N)
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
have := (stationaryPoint_spec hne' le_rfl hle).symm
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this : padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) = 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this :
  padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) =
    padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) N)
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this
no goals
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this : padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) = 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
simpa only [this]
no goals
case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : ¬stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
exact hN _ (lt_of_not_ge hle).le _ le_rfl