awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
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 - (↑(limSeq f i) : ℚ_[p])) < ε
have 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) sorry) :
        ℚ_[p])) <
  1 / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
Tactic: have h := Classical.choose_spec (rat_dense' (f i) (div_nat_pos i))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
have hε3 : 0 < ε / 3
Tactic: have hε3 : 0 < ε / 3 := div_pos hε (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
have 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) < ε
Tactic: let ⟨N, hN⟩ := exi_rat_seq_conv f hε3
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
have 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) < ε
Tactic: let ⟨N2, hN2⟩ := f.cauchy₂ hε3
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
have exists : ∀ j ≥ max N N2, padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
Tactic: exists max N N2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
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]))) <
    ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
have this₁ : (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (↑(limSeq f j) : ℚ_[p]) (↑(limSeq f (max N N2)) : ℚ_[p])) < ε
Tactic: ring_nf at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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])) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
have rw : (padicNormE : (a : ℚ_[p]) → ℚ) (↑(limSeq f j - limSeq f (max N N2)) : ℚ_[p]) < ε
Tactic: rw [← padicNormE.eq_padic_norm']
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
have padicNormE : (padicNormE : (a : ℚ_[p]) → ℚ)
    ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
      ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) <
  ε
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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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]))) <
    ε
have 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])) : ℚ)
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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])) : ℚ)
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2) +
        ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p]))) <
    ε
have 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])) : ℚ) <
  ε
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ 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])) : ℚ) <
    ε
have 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
Tactic: rw [← add_thirds ε]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ 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
have hbc : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3 + ε / 3
Tactic: apply _root_.add_lt_add
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ 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
have hbc₁ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) < ε / 3
Tactic: apply _root_.add_lt_add
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)) < ε / 3 + ε / 3
have hbc : (padicNormE : (a : ℚ_[p]) → ℚ)
    ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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))) <
    ε / 3 + ε / 3
have 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)) : ℚ)
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)) : ℚ)
⊢ (padicNormE : (a : ℚ_[p]) → ℚ)
      ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j + ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2))) <
    ε / 3 + ε / 3
have 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
Tactic: apply lt_of_le_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ 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
have hbc : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑(limSeq f j) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) j) < ε / 3
Tactic: apply _root_.add_lt_add
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ 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
have hbc₁ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) (max N N2)) < ε / 3
Tactic: apply _root_.add_lt_add
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) < ε / 3
have hbc : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑(limSeq f j) : ℚ_[p])) < ε / 3
Tactic: rw [padicNormE.map_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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 - (↑(limSeq f j) : ℚ_[p])) < ε / 3
have hbc : j ≥ N
Tactic: apply mod_cast hN j
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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]) (max N N2) - (↑(limSeq f (max N N2)) : ℚ_[p])) < ε / 3
have hbc : max N N2 ≥ N
Tactic: apply mod_cast hN (max N N2)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
ε : ℚ
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε
have 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) < ε
Tactic: obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε
have 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) < ε
Tactic: obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) < ε
have refine : ∀ (i : ℕ) (hi : i ≥ max N N2), (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑f : ℕ → ℚ_[p]) i) < ε
Tactic: refine ⟨max N N2, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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 - (↑f : ℕ → ℚ_[p]) i) < ε
have rw : (padicNormE : (a : ℚ_[p]) → ℚ)
    (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) + ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i)) <
  ε
Tactic: rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)) <
    ε
have refine : HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
    ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
  ε
Tactic: refine (padicNormE.add_le _ _).trans_lt ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε
have rw : HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
    ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
  ε / 2 + ε / 2
Tactic: rw [← add_halves ε]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε / 2 + ε / 2
have h₁ : (padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
Tactic: apply _root_.add_lt_add
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ HAdd.hAdd (α := ℚ) (β := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (lim f - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) : ℚ)
      ((padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) : ℚ) <
    ε / 2 + ε / 2
have h₂ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) < ε / 2
Tactic: apply _root_.add_lt_add
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) : ℕ → ℚ) i) : ℚ_[p]) - (↑f : ℕ → ℚ_[p]) i) < ε / 2
have h₂ : (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑((↑(lim' f) : ℕ → ℚ) i) : ℚ_[p])) < ε / 2
Tactic: rw [padicNormE.map_sub]