awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
obtain :
  ∀ (q : ℚ_[p])
    (hq :
      ∀ ε > 0,
        ∃ (N : ℕ),
          ∀ i ≥ N,
            (padicNormE : (a : ℚ_[p]) → ℚ)
                ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                          (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                      ℕ → ℚ_[p])
                    i -
                  q) <
              ε),
    ∃ (b : ℚ_[p]), f ≈ const norm b
⊢ ∃ (b : ℚ_[p]), f ≈ const norm b

Tactic:
obtain ⟨q, hq⟩ := Padic.complete'' ⟨f, cau_seq_norm_e⟩

Premises used: Subtype.mk, Padic.complete'', Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
exists : f ≈ const norm q
⊢ ∃ (b : ℚ_[p]), f ≈ const norm b

Tactic:
exists q
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
obtain :
  ∀ (ε' : ℚ) (hε' : LT.lt (α := ℝ) 0 (↑ε' : ℝ) ∧ (↑ε' : ℝ) < ε),
    ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε

Tactic:
obtain ⟨ε', hε'⟩ := exists_rat_btwn hε

Premises used: exists_rat_btwn
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : LT.lt (α := ℝ) 0 (↑ε' : ℝ) ∧ (↑ε' : ℝ) < ε
⊢ 0 < ε' ∧ (↑ε' : ℝ) < ε

Tactic:
norm_cast at hε'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
obtain :
  ∀ (N : ℕ)
    (hN :
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε'),
    ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε

Tactic:
obtain ⟨N, hN⟩ := hq ε' hε'.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
exists : ∀ j ≥ N, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε

Tactic:
exists N
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'

Tactic:
have h := hN i hi
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
change : ‖(↑f : ℕ → ℚ_[p]) i - q‖ < ε
⊢ ‖(↑(f - const norm q) : ℕ → ℚ_[p]) i‖ < ε

Tactic:
change norm (f i - q) < ε

Premises used: Norm.norm, HSub.hSub, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
⊢ ‖(↑f : ℕ → ℚ_[p]) i - q‖ < ε

Tactic:
lt_trans ?_ hε'.2

Premises used: lt_trans, And.right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
refine : ‖(↑f : ℕ → ℚ_[p]) i - q‖ < (↑ε' : ℝ)
⊢ ‖(↑f : ℕ → ℚ_[p]) i - q‖ < ε

Tactic:
refine lt_trans ?_ hε'.2

Premises used: lt_trans, And.right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
dsimp : LT.lt (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q)) : ℝ) (↑ε' : ℝ)
⊢ ‖(↑f : ℕ → ℚ_[p]) i - q‖ < (↑ε' : ℝ)

Tactic:
dsimp [norm]

Premises used: Norm.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
⊢ LT.lt (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q)) : ℝ) (↑ε' : ℝ)

Tactic:
mod_cast h

Premises used: cast, Rat.cast_lt._simp_1, Eq.symm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ (↑ε' : ℝ) < ε
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                  cau_seq_norm_e) :
              ℕ → ℚ_[p])
            i -
          q) <
      ε'
i : ℕ
hi : i ≥ N
h :
  (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f) (↑f : ℕ → ℚ_[p])
                cau_seq_norm_e) :
            ℕ → ℚ_[p])
          i -
        q) <
    ε'
⊢ LT.lt (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q)) : ℝ) (↑ε' : ℝ)

Tactic:
exact mod_cast h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a), ‖f.lim‖ ≤ a
⊢ ‖f.lim‖ ≤ a

Tactic:
obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ ha

Premises used: CauSeq.equiv_lim, Setoid.symm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a
⊢ ‖f.lim‖ = ‖f.lim - (↑f : ℕ → ℚ_[p]) N + (↑f : ℕ → ℚ_[p]) N‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a
⊢ ‖f.lim - (↑f : ℕ → ℚ_[p]) N + (↑f : ℕ → ℚ_[p]) N‖ ≤ max ‖f.lim - (↑f : ℕ → ℚ_[p]) N‖ ‖(↑f : ℕ → ℚ_[p]) N‖

Tactic:
nonarchimedean _ _

Premises used: Padic.nonarchimedean
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a
⊢ max ‖f.lim - (↑f : ℕ → ℚ_[p]) N‖ ‖(↑f : ℕ → ℚ_[p]) N‖ ≤ a

Tactic:
max_le (le_of_lt (hN _ le_rfl)) (hf _)

Premises used: le_rfl, le_of_lt, max_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖(↑f : ℕ → ℚ_[p]) i‖ ≤ a
N : ℕ
hN : ∀ j ≥ N, ‖(↑(const norm f.lim - f) : ℕ → ℚ_[p]) j‖ < a
f₁ : ‖f.lim‖ = ‖f.lim - (↑f : ℕ → ℚ_[p]) N + (↑f : ℕ → ℚ_[p]) N‖
⊢ ‖f.lim‖ ≤ a

Tactic:
calc
    ‖f.lim‖ = ‖f.lim - f N + f N‖ := by simp
    _ ≤ max ‖f.lim - f N‖ ‖f N‖ := nonarchimedean _ _
    _ ≤ a := max_le (le_of_lt (hN _ le_rfl)) (hf _)

Premises used: Norm.norm, le_rfl, HSub.hSub, le_of_lt, Max.max, CauSeq.lim, Padic.nonarchimedean, max_le, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ∀ (u : ℕ → ℚ_[p]), CauchySeq u → ∃ (a : ℚ_[p]), Tendsto u atTop (nhds a)
⊢ CompleteSpace ℚ_[p]

Tactic:
apply complete_of_cauchySeq_tendsto

Premises used: Metric.complete_of_cauchySeq_tendsto
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
⊢ ∃ (a : ℚ_[p]), Tendsto u atTop (nhds a)

Tactic:
⟨c.lim, fun s h ↦ ?_⟩

Premises used: CauSeq.lim, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
a : ∀ (s : Set ℚ_[p]) (h : s ∈ nhds c.lim), s ∈ Filter.map u atTop
⊢ ∃ (a : ℚ_[p]), Tendsto u atTop (nhds a)

Tactic:
refine ⟨c.lim, fun s h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
a : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball c.lim ε ⊆ s), s ∈ Filter.map u atTop
⊢ s ∈ Filter.map u atTop

Tactic:
rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩

Premises used: Metric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(c - const norm c.lim) : ℕ → ℚ_[p]) j‖ < ε

Tactic:
have := c.equiv_lim ε ε0
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(c - const norm c.lim) : ℕ → ℚ_[p]) j‖ < ε
a : ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s
⊢ s ∈ Filter.map u atTop

Tactic:
simp only [mem_map, mem_atTop_sets]

Premises used: Filter.mem_atTop_sets, Filter.mem_map
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(c - const norm c.lim) : ℕ → ℚ_[p]) j‖ < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s

Tactic:
this.imp fun N hN n hn ↦ hε (hN n hn)

Premises used: Exists.imp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq norm f) u ⋯
s : Set ℚ_[p]
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(c - const norm c.lim) : ℕ → ℚ_[p]) j‖ < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, b ∈ u ⁻¹' s

Tactic:
exact this.imp fun N hN n hn ↦ hε (hN n hn)

Premises used: Exists.imp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
pos : ∀ (hf : f ≈ 0), PadicSeq.valuation f = PadicSeq.valuation g
neg : ∀ (hf : ¬f ≈ 0), PadicSeq.valuation f = PadicSeq.valuation g
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
by_cases hf : f ≈ 0
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : f ≈ 0
⊢ g ≈ 0

Tactic:
have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
simp [hf, hg, PadicSeq.valuation]

Premises used: PadicSeq.valuation
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ ¬g ≈ 0

Tactic:
have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
neg : PadicSeq.norm f = PadicSeq.norm g
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
rw [PadicSeq.val_eq_iff_norm_eq hf hg]

Premises used: PadicSeq.val_eq_iff_norm_eq
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.norm f = PadicSeq.norm g

Tactic:
PadicSeq.norm_equiv h

Premises used: PadicSeq.norm_equiv
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.norm f = PadicSeq.norm g

Tactic:
exact PadicSeq.norm_equiv h

Premises used: PadicSeq.norm_equiv
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) 0 = 0

Tactic:
dif_pos ((const_equiv p).2 rfl)

Premises used: PadicSeq.valuation, Iff.mpr, dif_pos, Padic.valuation, Padic.const_equiv, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
h :
  ∀ (f : CauSeq ℚ (padicNorm p)),
    Ne (α := ℚ_[p]) ⟦f⟧ 0 → norm (E := ℚ_[p]) ⟦f⟧ = HPow.hPow (α := ℝ) (↑p : ℝ) (-valuation ⟦f⟧)
⊢ x ≠ 0 → ‖x‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation)

Tactic:
induction x using Quotient.inductionOn with | _ f
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
h : (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-PadicSeq.valuation f)) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
h₁ : ¬f ≈ 0
⊢ (↑(PadicSeq.norm f) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)

Tactic:
rw [PadicSeq.norm_eq_zpow_neg_valuation]

Premises used: PadicSeq.norm_eq_zpow_neg_valuation
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
h : HPow.hPow (α := ℝ) (↑(↑p : ℚ) : ℝ) (-PadicSeq.valuation f) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
h₁ h₂ : HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)
⊢ (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-PadicSeq.valuation f)) : ℝ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-PadicSeq.valuation f)

Tactic:
rw [Rat.cast_zpow, Rat.cast_natCast]

Premises used: Rat.cast_natCast, Rat.cast_zpow
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
h : ¬f - 0 ≈ 0
⊢ ¬f ≈ 0

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero

Premises used: CauSeq.not_limZero_of_not_congr_zero
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
h : ∀ (hf : f - 0 ≈ 0), Eq (α := ℚ_[p]) ⟦f⟧ 0
⊢ ¬f - 0 ≈ 0

Tactic:
contrapose hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : f - 0 ≈ 0
h : f ≈ const (padicNorm p) 0
⊢ Eq (α := ℚ_[p]) ⟦f⟧ 0

Tactic:
apply Quotient.sound

Premises used: Quotient.sound
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : f - 0 ≈ 0
⊢ f ≈ const (padicNorm p) 0

Tactic:
simpa using hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
inl : valuation (p := p) (↑0 : ℚ_[p]) = padicValRat p 0
inr : ∀ (hq : q ≠ 0), valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q
⊢ valuation (p := p) (↑q : ℚ_[p]) = padicValRat p q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) (↑0 : ℚ_[p]) = padicValRat p 0

Tactic:
simp only [Rat.cast_zero, valuation_zero, padicValRat.zero]

Premises used: padicValRat.zero, Padic.valuation_zero, Rat.cast_zero