awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
⊢ (f + g).norm = max f.norm g.norm
have have : ∀ (hfg : ¬f + g ≈ 0), (f + g).norm = max f.norm g.norm
Tactic: classical
  have hfg : ¬f + g ≈ 0 := mt norm_eq_of_add_equiv_zero hfgne
  exact if hf : f ≈ 0 then by
    have : LimZero (f - 0) := hf
    have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
    have h1 : (f + g).norm = g.norm := norm_equiv this
    have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
    rw [h1, h2, max_eq_right (norm_nonneg _)]
  else
    if hg : g ≈ 0 then by
      have : LimZero (g - 0) := hg
      have : f + g ≈ f := show LimZero (f + g - f) by simpa only [add_sub_cancel_left, sub_zero]
      have h1 : (f + g).norm = f.norm := norm_equiv this
      have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
      rw [h1, h2, max_eq_left (norm_nonneg _)]
    else by
      unfold norm at hfgne ⊢; split_ifs at hfgne ⊢
      -- Porting note: originally `padic_index_simp [hfg, hf, hg] at hfgne ⊢`
      rw [lift_index_left hf, lift_index_right hg] at hfgne
      · rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
        exact padicNorm.add_eq_max_of_ne hfgne
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
⊢ HasEquiv.Equiv (α := CauSeq ℚ (padicNorm p)) (const (padicNorm p) q) (const (padicNorm p) r)
have rw : (equiv : CauSeq ℚ (padicNorm p) → CauSeq ℚ (padicNorm p) → Prop) (const (padicNorm p) r) (const (padicNorm p) r)
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q r : ℚ
h : q = r
⊢ Eq (α := ℚ_[p]) (↑q : ℚ_[p]) (↑r : ℚ_[p])
have rw : Eq (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r : ℚ_[p])
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
m n : ℕ
⊢ Eq (α := ℚ_[p]) (↑(↑m : ℚ) : ℚ_[p]) (↑n : ℚ_[p]) → m = n
have norm_cast : m = n → m = n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔ Eq (α := ℚ_[p]) ⟦r⟧ 0
have erw : Quotient.lift (s := equiv) PadicSeq.norm sorry ⟦r⟧ = 0 ↔
  (equiv : CauSeq ℚ (padicNorm p) → CauSeq ℚ (padicNorm p) → Prop) r 0
Tactic: erw [Padic.zero_def, Quotient.eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r
have max : Quotient.lift PadicSeq.norm sorry (q + r) ≤ max (Quotient.lift PadicSeq.norm sorry q) (Quotient.lift PadicSeq.norm sorry r)
Tactic: trans
      max ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) q)
        ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) r)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
max :
  Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ Max.max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r)
⊢ Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r
have max₁ : Max.max (Quotient.lift PadicSeq.norm sorry q) (Quotient.lift PadicSeq.norm sorry r) ≤
  Quotient.lift PadicSeq.norm sorry q + Quotient.lift PadicSeq.norm sorry r
Tactic: trans
      max ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) q)
        ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) r)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r)
have h : ∀ (a b : CauSeq ℚ (padicNorm p)),
  Quotient.lift PadicSeq.norm sorry (HAdd.hAdd (α := ℚ_[p]) ⟦a⟧ ⟦b⟧) ≤
    max (Quotient.lift (s := equiv) PadicSeq.norm sorry ⟦a⟧) (Quotient.lift (s := equiv) PadicSeq.norm sorry ⟦b⟧)
Tactic: induction q, r using Quotient.inductionOn₂
Cleared hypotheses: q, r
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r) ≤
    Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r
have ha : 0 ≤ Quotient.lift PadicSeq.norm sorry q
Tactic: apply max_le_add_of_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
ha : 0 ≤ Quotient.lift PadicSeq.norm ⋯ q
⊢ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r) ≤
    Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r
have hb : 0 ≤ Quotient.lift PadicSeq.norm sorry r
Tactic: apply max_le_add_of_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ q
have ha : ∀ (a : CauSeq ℚ (padicNorm p)), 0 ≤ Quotient.lift (s := equiv) PadicSeq.norm sorry ⟦a⟧
Tactic: induction q using Quotient.inductionOn
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ r
have hb : ∀ (a : CauSeq ℚ (padicNorm p)), 0 ≤ Quotient.lift (s := equiv) PadicSeq.norm sorry ⟦a⟧
Tactic: induction r using Quotient.inductionOn
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ (N : ℕ), ∀ i ≥ N, (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε
⊢ ∃ (N : ℕ),
    ∀ i ≥ N, Quotient.lift PadicSeq.norm ⋯ (HSub.hSub (α := ℚ_[p]) (Padic.mk f) (↑((↑f : ℕ → ℚ) i) : ℚ_[p])) < ε
have h : ∀ (N i : ℕ),
  i ≥ N →
    ∀ (N : (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε),
      Quotient.lift PadicSeq.norm sorry (HSub.hSub (α := ℚ_[p]) (Padic.mk f) (↑((↑f : ℕ → ℚ) i) : ℚ_[p])) < ε
Tactic: peel hyp with N
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε
have by_contra! : ∀ (h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
⊢ False
have obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε), False
Tactic: obtain ⟨N, hN⟩ := cauchy₂ f hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
⊢ False
have rcases : ∀ (i : ℕ) (hi : i ≥ N) (hge : ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm), False
Tactic: rcases h N with ⟨i, hi, hge⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h_1 : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
h : f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
⊢ False
have hge₁ : ε ≤ 0
Tactic: rw [PadicSeq.norm, dif_pos h] at hge
Cleared hypotheses: hge, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
⊢ False
have hne : ¬f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
Tactic: have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := fun h ↦ by
    rw [PadicSeq.norm, dif_pos h] at hge
    exact not_lt_of_ge hge hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hge :
  ε ≤
    if hf : f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0 then 0
    else padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hf))
hne : ¬f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
⊢ False
have hge₁ : ε ≤ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
Tactic: split_ifs at hge
Cleared hypotheses: hge
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
hge : ε ≤ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
⊢ False
have apply : padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε
Tactic: apply not_le_of_gt _ hge
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
hge : ε ≤ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
hngen : stationaryPoint hne ≤ N
⊢ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε
have this : padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) N) =
  padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
Tactic: have := stationaryPoint_spec hne le_rfl hngen
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
hge : ε ≤ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
hngen : stationaryPoint hne ≤ N
this :
  padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) N) =
    padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
⊢ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε
have inr : padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) N) < ε
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
hge : ε ≤ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))
⊢ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε
have x : N ≤ stationaryPoint hne ∨ stationaryPoint hne ≤ N
Tactic: cases _root_.le_total N (stationaryPoint hne) with
  | inl hgen =>
    exact hN _ hgen _ hi
  | inr hngen =>
    have := stationaryPoint_spec hne le_rfl hngen
    rw [← this]
    exact hN _ le_rfl _ hi
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) < ε
⊢ (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
have inl : ∀ (heq : q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
Tactic: rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) < ε
inl : ∀ (heq : q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
⊢ (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
have inr : ∀ (hne' : ¬q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
Tactic: rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
have inr : padicNorm p ((↑(q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)) : ℕ → ℚ) (stationaryPoint hne')) < ε
Tactic: simp only [PadicSeq.norm, dif_neg hne']
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ padicNorm p ((↑(q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)) : ℕ → ℚ) (stationaryPoint hne')) < ε
have inr : padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
Tactic: change padicNorm p (q' _ - q' _) < ε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
have inr : ∀ (hle : stationaryPoint hne' ≤ N), padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
Tactic: rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) < ε
⊢ padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
have inr₁ : ∀ (hle : ¬stationaryPoint hne' ≤ N), padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) < ε
Tactic: rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
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) < ε
have this₁ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
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) < ε
have this₁ : padicNorm p ((↑q' : ℕ → ℚ) (stationaryPoint hne') - (↑q' : ℕ → ℚ) N) = 0
Tactic: simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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) < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) ⟦q'⟧ (↑((↑q' : ℕ → ℚ) N) : ℚ_[p])) < ε
have dsimp : Quotient.lift PadicSeq.norm sorry (HSub.hSub (α := ℚ_[p]) (Completion.mk 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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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])) < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) ⟦q'⟧ (↑((↑q' : ℕ → ℚ) N) : ℚ_[p])) < ε
have dsimp₁ : (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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 < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) ⟦q'⟧ (↑((↑q' : ℕ → ℚ) N) : ℚ_[p])) < ε
have inl : ∀ (heq : q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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 < ε
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) ⟦q'⟧ (↑((↑q' : ℕ → ℚ) N) : ℚ_[p])) < ε
have inr : ∀ (hne' : ¬q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
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
-- 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]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε
have refine : ∀ (N : ℕ) (hN : 1 / ε < (↑N : ℚ)) (i : ℕ) (hi : i ≥ N),
  (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - (↑(limSeq f i) : ℚ_[p])) < ε
Tactic: refine (exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ ?_