awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
hne' : ¬q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0
inr : ∀ (hle : stationaryPoint hne' ≤ N), padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
inr₁ : ∀ (hle : ¬stationaryPoint hne' ≤ N), padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
⊢ padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε

Tactic:
rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle

Premises used: PadicSeq.stationaryPoint, LE.le, Decidable.em
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
hne' : ¬q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0
hle : stationaryPoint hne' ≤ N
⊢ padicNorm p ((↑(q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)) : ℕ → ℚ) (stationaryPoint hne')) =
    padicNorm p ((↑(q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)) : ℕ → ℚ) N)

Tactic:
have := (stationaryPoint_spec hne' le_rfl hle).symm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this_1 : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ 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) = 0

Tactic:
simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this

Premises used: sub_self, CauSeq.sub_apply, CauSeq.const_apply, padicNorm.zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this_1 : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ 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) < ε

Tactic:
simpa only [this]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ 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) < ε

Tactic:
hN _ (lt_of_not_ge hle).le _ le_rfl

Premises used: le_rfl, lt_of_not_ge, LT.lt.le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ 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) < ε

Tactic:
exact hN _ (lt_of_not_ge hle).le _ le_rfl

Premises used: le_rfl, lt_of_not_ge, LT.lt.le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
dsimp : Quotient.lift PadicSeq.norm ⋯ (HSub.hSub (α := ℚ_[p]) (Completion.mk q') (↑((↑q' : ℕ → ℚ) N) : ℚ_[p])) < ε
dsimp₁ : (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
inl : ∀ (heq : q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
inr inr₁ :
  ∀ (hne' : ¬q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) ⟦q'⟧ (↑((↑q' : ℕ → ℚ) N) : ℚ_[p])) < ε

Tactic:
classical
      dsimp [padicNormE]
      convert_to PadicSeq.norm (q' - const _ (q' N)) < ε -- `change` times out here.
      rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
      · simpa only [heq, PadicSeq.norm, dif_pos]
      · simp only [PadicSeq.norm, dif_neg hne']
        change padicNorm p (q' _ - q' _) < ε
        rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
        · have := (stationaryPoint_spec hne' le_rfl hle).symm
          simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this
          simpa only [this]
        · exact hN _ (lt_of_not_ge hle).le _ le_rfl

Premises used: padicNormE, sub_self, HSub.hSub, CauSeq.sub_apply, dif_pos, CauSeq.const_apply, CauSeq.const, padicNorm, padicNorm.zero, Subtype.val, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
n : ℕ
⊢ 0 < 1 / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1

Tactic:
div_pos zero_lt_one (mod_cast succ_pos _)

Premises used: congrArg, Nat.cast_lt._simp_1, Nat.cast_add._simp_1, cast, Nat.cast, zero_lt_one, HAdd.hAdd, Nat.succ_pos, congr, LT.lt, div_pos, Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : 0 < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε

Tactic:
(exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ ?_

Premises used: HDiv.hDiv, Exists.imp, exists_nat_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : 0 < ε
refine :
  ∀ (N : ℕ) (hN : 1 / ε < (↑N : ℚ)) (i : ℕ) (hi : i ≥ N),
    (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε

Tactic:
refine (exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ ?_

Premises used: HDiv.hDiv, Exists.imp, exists_nat_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < (↑N : ℚ)
i : ℕ
hi : i ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑f : ℕ → ℚ_[p]) i -
        (↑(Classical.choose (p := fun (x : ℚ) ↦
              (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑x : ℚ_[p])) < 1 / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)
              ⋯) :
          ℚ_[p])) <
    1 / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1

Tactic:
have h := Classical.choose_spec (rat_dense' (f i) (div_nat_pos i))
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < (↑N : ℚ)
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑f : ℕ → ℚ_[p]) i -
        (↑(Classical.choose (p := fun (x : ℚ) ↦
              (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑x : ℚ_[p])) < 1 / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)
              ⋯) :
          ℚ_[p])) <
    1 / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε

Tactic:
lt_of_lt_of_le h ((div_le_iff₀' <| mod_cast succ_pos _).mpr ?_)

Premises used: Iff.mpr, div_le_iff₀', lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
⊢ LT.lt (α := ℚ) 0 3

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
⊢ 0 < ε / 3

Tactic:
have hε3 : 0 < ε / 3 := div_pos hε (by simp)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
let :
  ∀ (N : ℕ) (hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3),
    ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε

Tactic:
let ⟨N, hN⟩ := exi_rat_seq_conv f hε3
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
let :
  ∀ (N2 : ℕ)
    (hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3),
    ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε

Tactic:
let ⟨N2, hN2⟩ := f.cauchy₂ hε3
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
exists : ∀ j ≥ max N N2, padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε

Tactic:
exists max N N2

Premises used: Max.max
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
        ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) <
    ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (↑(limSeq f j) : ℚ_[p]) (↑(limSeq f (max N N2)) : ℚ_[p])) < ε

Tactic:
ring_nf at this
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this :
  (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (↑(limSeq f j) : ℚ_[p]) (↑(limSeq f (max N N2)) : ℚ_[p])) < ε
rw : (padicNormE : (a : ℚ_[p]) → ℚ) (↑(limSeq f j - limSeq f (max N N2)) : ℚ_[p]) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
rw [← padicNormE.eq_padic_norm']

Premises used: padicNormE.eq_padic_norm'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this :
  (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (↑(limSeq f j) : ℚ_[p]) (↑(limSeq f (max N N2)) : ℚ_[p])) < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (↑(limSeq f j - limSeq f (max N N2)) : ℚ_[p]) < ε

Tactic:
mod_cast this

Premises used: padicNormE, congrArg, cast, Rat.cast_sub._simp_1, Max.max, LT.lt, congrFun', Padic.limSeq, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this :
  (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (↑(limSeq f j) : ℚ_[p]) (↑(limSeq f (max N N2)) : ℚ_[p])) < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (↑(limSeq f j - limSeq f (max N N2)) : ℚ_[p]) < ε

Tactic:
exact mod_cast this
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑_root_.padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (_root_.padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (_root_.padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
padicNormE :
  (_root_.padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
        ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) <
    ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε

Tactic:
suffices
    padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε by
    ring_nf at this
    rw [← padicNormE.eq_padic_norm']
    exact mod_cast this
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hab :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
        ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) ≤
    HAdd.hAdd (α := ℚ) (β := ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) : ℚ)
hbc :
  HAdd.hAdd (α := ℚ) (β := ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) : ℚ) <
    ε
b : ℚ
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
        ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) <
    ε

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
        ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) ≤
    HAdd.hAdd (α := ℚ) (β := ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) : ℚ)

Tactic:
apply padicNormE.add_le

Premises used: padicNormE, AbsoluteValue.add_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc :
  HAdd.hAdd (α := ℚ) (β := ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) : ℚ) <
    ε / 3 + ε / 3 + ε / 3
⊢ HAdd.hAdd (α := ℚ) (β := ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) : ℚ) <
    ε

Tactic:
rw [← add_thirds ε]

Premises used: add_thirds
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3 + ε / 3
hbc₁ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) < ε / 3
⊢ HAdd.hAdd (α := ℚ) (β := ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) : ℚ) <
    ε / 3 + ε / 3 + ε / 3

Tactic:
apply _root_.add_lt_add

Premises used: add_lt_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2))) <
    ε / 3 + ε / 3
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3 + ε / 3

Tactic:
simpa only [sub_add_sub_cancel]

Premises used: sub_add_sub_cancel
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2))) <
    ε / 3 + ε / 3
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3 + ε / 3

Tactic:
suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
        simpa only [sub_add_sub_cancel]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2))) ≤
    HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)
hbc₁ :
  HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ) <
    ε / 3 + ε / 3
hbc₂ : ℚ
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2))) <
    ε / 3 + ε / 3

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2))) ≤
    HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ)

Tactic:
apply padicNormE.add_le

Premises used: padicNormE, AbsoluteValue.add_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) < ε / 3
hbc₁ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3
⊢ HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) : ℚ) <
    ε / 3 + ε / 3

Tactic:
apply _root_.add_lt_add

Premises used: add_lt_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑(limSeq f j) : ℚ_[p])) < ε / 3
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) < ε / 3

Tactic:
rw [padicNormE.map_sub]

Premises used: padicNormE, AbsoluteValue.map_sub
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) k) < ε / 3
j : ℕ
hj : j ≥ max N N2
hbc : j ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑(limSeq f j) : ℚ_[p])) < ε / 3

Tactic:
apply mod_cast hN j