awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ j ≥ N

Tactic:
le_of_max_le_left hj

Premises used: le_of_max_le_left
-- 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
⊢ j ≥ N

Tactic:
exact le_of_max_le_left hj

Premises used: le_of_max_le_left
-- 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]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3

Tactic:
hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)

Premises used: le_max_right, le_of_max_le_right
-- 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]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3

Tactic:
exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)

Premises used: le_max_right, le_of_max_le_right
-- 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 : max N N2 ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) < ε / 3

Tactic:
apply mod_cast hN (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
⊢ max N N2 ≥ N

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
obtain :
  ∀ (N : ℕ) (hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2),
    ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε

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

Premises used: half_pos, Padic.exi_rat_seq_conv
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
obtain :
  ∀ (N2 : ℕ)
    (hN2 :
      ∀ i ≥ N2,
        (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) <
          ε / 2),
    ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε

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

Premises used: half_pos, _private.0.Padic.lim', padicNormE.defn
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε

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

Premises used: Max.max, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
refine : ∀ (i : ℕ) (hi : i ≥ max N N2), (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε

Tactic:
refine ⟨max N N2, fun i hi ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
rw :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) + ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i)) <
    ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε

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

Premises used: sub_add_sub_cancel, _private.0.Padic.lim', Rat.cast, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) + ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i)) <
    ε

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

Premises used: padicNormE, AbsoluteValue.add_le, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
refine :
  HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) + ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i)) <
    ε

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

Premises used: padicNormE, AbsoluteValue.add_le, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
rw :
  HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε / 2 + ε / 2
⊢ HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε

Tactic:
rw [← add_halves ε]

Premises used: add_halves
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
h₁ : (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
h₂ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) < ε / 2
⊢ HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε / 2 + ε / 2

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
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2

Tactic:
apply hN2 _ (le_of_max_le_right hi)

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

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
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε / 2
N2 : ℕ
hN2 :
  ∀ i ≥ N2,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk (lim' f)) (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2

Tactic:
hN _ (le_of_max_le_left hi)

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

Tactic:
exact hN _ (le_of_max_le_left hi)

Premises used: le_of_max_le_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
obtain :
  ∀ (x : ℚ_[p]) (hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε),
    ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε
⊢ ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε

Tactic:
obtain ⟨x, hx⟩ := complete' f

Premises used: Padic.complete'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε

Tactic:
⟨x, fun ε hε => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
refine : ∀ (ε : ℚ) (hε : ε > 0), ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
⊢ ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε

Tactic:
refine ⟨x, fun ε hε => ?_⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
obtain :
  ∀ (N : ℕ) (hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε),
    ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε

Tactic:
obtain ⟨N, hN⟩ := hx ε hε
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε

Tactic:
⟨N, fun i hi => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
refine : ∀ (i : ℕ) (hi : i ≥ N), (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε

Tactic:
refine ⟨N, fun i hi => ?_⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
i : ℕ
hi : i ≥ N
rw : (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε

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]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
i : ℕ
hi : i ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε

Tactic:
hN i hi
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
i : ℕ
hi : i ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε

Tactic:
exact hN i hi
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ dist x z ≤ max (dist x y) (dist y z)

Tactic:
simpa [dist] using padicNormE.nonarchimedean' (x - y) (y - z)

Premises used: padicNormE.nonarchimedean', HSub.hSub, Dist.dist
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ ∀ (x : ℚ_[p]), dist x x = 0

Tactic:
simp [dist]

Premises used: Dist.dist
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = dist y x

Tactic:
simp [dist, ← padicNormE.map_neg (x - y : ℚ_[p])]

Premises used: AbsoluteValue.map_neg, padicNormE, HSub.hSub, Dist.dist
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - z)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (y - z)) : ℝ)

Tactic:
mod_cast padicNormE.sub_le x y z

Premises used: padicNormE, Rat.cast_add._simp_1, congrArg, HSub.hSub, cast, Rat.cast, LE.le, AbsoluteValue.sub_le, Eq.symm, DFunLike.coe, Rat.cast_le._simp_1, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - z)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (y - z)) : ℝ)

Tactic:
exact mod_cast padicNormE.sub_le x y z

Premises used: padicNormE, AbsoluteValue.sub_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ_[p]
_ : ∀ {y : ℚ_[p]}, Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0 → x = y
⊢ ∀ {y : ℚ_[p]}, Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0 → x = y

Tactic:
_
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
h : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0
h₁ : x - y = 0
⊢ x = y

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
h : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0
h₁ : Eq (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (x - y) : ℚ) (0 : ℚ)
⊢ x - y = 0

Tactic:
apply padicNormE.eq_zero.1

Premises used: AbsoluteValue.eq_zero, padicNormE, Iff.mp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
h : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0
⊢ Eq (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (x - y) : ℚ) (0 : ℚ)

Tactic:
mod_cast h

Premises used: padicNormE, congrArg, Rat.cast_inj._simp_1, HSub.hSub, cast, Rat.cast, Rat.cast_zero, Nat.cast_zero, Eq.symm, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
h : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0
⊢ Eq (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (x - y) : ℚ) (0 : ℚ)

Tactic:
exact mod_cast h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
rw : dist x y = ‖y - x‖
⊢ dist x y = ‖-x + y‖

Tactic:
rw [add_comm, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
change : ‖x - y‖ = ‖y - x‖
⊢ dist x y = ‖y - x‖

Tactic:
change ‖x - y‖ = ‖y - x‖
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ y - x = -1 * (x - y)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ y - x = -1 * (x - y)

Tactic:
have : y - x = (-1) * (x - y) := by ring
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
this : y - x = -1 * (x - y)
⊢ ‖x - y‖ = ‖y - x‖

Tactic:
simp only [this, Norm.norm, map_mul, map_neg_eq_map, AbsoluteValue.map_one, one_mul]

Premises used: Norm.norm, AddGroupSeminormClass.map_neg_eq_map, map_mul, one_mul, AbsoluteValue.map_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ ∀ (a b : ℚ_[p]), ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
simp [Norm.norm, map_mul]

Premises used: Norm.norm, map_mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ_[p]), ‖x * y‖ = ‖x‖ * ‖y‖

Tactic:
simp [Norm.norm, map_mul]

Premises used: Norm.norm, map_mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : LT.lt (α := ℝ) 0 (↑ε' : ℝ)
hε'r : (↑ε' : ℝ) < ε
⊢ 0 < ε'

Tactic:
simpa using hε'l
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : LT.lt (α := ℝ) 0 (↑ε' : ℝ)
hε'r : (↑ε' : ℝ) < ε
r : ℚ
hr : (padicNormE : (a : ℚ_[p]) → ℚ) (q - (↑r : ℚ_[p])) < ε'
⊢ ‖q - (↑r : ℚ_[p])‖ < (↑ε' : ℝ)

Tactic:
simpa [Norm.norm] using hr

Premises used: Norm.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ_[p]
rw : ∀ ε > 0, ∃ (k : ℚ), dist x (↑k : ℚ_[p]) < ε
⊢ Membership.mem (γ := Set ℚ_[p]) (closure (Set.range Rat.cast)) x

Tactic:
rw [Metric.mem_closure_range_iff]

Premises used: Metric.mem_closure_range_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ∀ ε > 0, ∃ (k : ℚ), dist x (↑k : ℚ_[p]) < ε

Tactic:
fun _ ↦ Padic.rat_dense _ x

Premises used: Padic.rat_dense
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ∀ ε > 0, ∃ (k : ℚ), dist x (↑k : ℚ_[p]) < ε

Tactic:
exact fun _ ↦ Padic.rat_dense _ x

Premises used: Padic.rat_dense
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q * r‖ = ‖q‖ * ‖r‖

Tactic:
simp [Norm.norm, map_mul]

Premises used: Norm.norm, map_mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) = ‖q‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ LE.le (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (q + r)) : ℝ)
    (max (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ))

Tactic:
mod_cast padicNormE.nonarchimedean' _ _

Premises used: padicNormE.nonarchimedean', padicNormE, Rat.cast_max._simp_1, congrArg, cast, Rat.cast, LE.le, HAdd.hAdd, Eq.symm, DFunLike.coe, Rat.cast_le._simp_1, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ LE.le (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (q + r)) : ℝ)
    (max (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ))

Tactic:
exact mod_cast padicNormE.nonarchimedean' _ _

Premises used: padicNormE.nonarchimedean'