awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
⊢ (f + g).norm = max f.norm g.norm

Tactic:
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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
have have₁ have₂ : ∀ (hfg : ¬f + g ≈ 0), (f + g).norm = max f.norm g.norm
⊢ (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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ℚ_[p]) 0 ⟦0⟧

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, CauSeq.Completion.mk, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ Eq (α := ℚ_[p]) (mk f) (mk g) ↔ f ≈ g

Tactic:
Quotient.eq'

Premises used: Padic.mk, CauSeq.Completion.Cauchy, Quotient.eq', Padic
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
rw rw₁ :
  (equiv : CauSeq ℚ (padicNorm p) → CauSeq ℚ (padicNorm p) → Prop) (const (padicNorm p) r) (const (padicNorm p) r)
⊢ HasEquiv.Equiv (α := CauSeq ℚ (padicNorm p)) (const (padicNorm p) q) (const (padicNorm p) r)

Tactic:
rw [heq]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q r : ℚ
h : q = r
rw rw₁ : Eq (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r : ℚ_[p])
⊢ Eq (α := ℚ_[p]) (↑q : ℚ_[p]) (↑r : ℚ_[p])

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
m n : ℕ
norm_cast : m = n → m = n
⊢ Eq (α := ℚ_[p]) (↑(↑m : ℚ) : ℚ_[p]) (↑n : ℚ_[p]) → m = n

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
m n : ℕ
⊢ m = n → m = n

Tactic:
id

Premises used: id
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
m n : ℕ
⊢ m = n → m = n

Tactic:
exact id

Premises used: id
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
⊢ (↑(x + y) : ℚ_[p]) = HAdd.hAdd (α := ℚ_[p]) (↑x : ℚ_[p]) (↑y : ℚ_[p])

Tactic:
Rat.cast_add _ _

Premises used: Rat.cast_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
⊢ Eq (α := ℚ_[p]) (↑(-x) : ℚ_[p]) (-(↑x : ℚ_[p]))

Tactic:
Rat.cast_neg _

Premises used: Rat.cast_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
⊢ (↑(x * y) : ℚ_[p]) = HMul.hMul (α := ℚ_[p]) (↑x : ℚ_[p]) (↑y : ℚ_[p])

Tactic:
Rat.cast_mul _ _

Premises used: Rat.cast_mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
⊢ (↑(x - y) : ℚ_[p]) = HSub.hSub (α := ℚ_[p]) (↑x : ℚ_[p]) (↑y : ℚ_[p])

Tactic:
Rat.cast_sub _ _

Premises used: Rat.cast_sub
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
⊢ (↑(x / y) : ℚ_[p]) = HDiv.hDiv (α := ℚ_[p]) (↑x : ℚ_[p]) (↑y : ℚ_[p])

Tactic:
Rat.cast_div _ _

Premises used: Rat.cast_div
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ℚ_[p]) (↑1 : ℚ_[p]) 1

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, CauSeq.Completion.mk, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ℚ_[p]) (↑0 : ℚ_[p]) 0

Tactic:
rfl

Premises used: CauSeq.Completion.ofRat, CauSeq.Completion.mk, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
erw :
  Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔
    (equiv : CauSeq ℚ (padicNorm p) → CauSeq ℚ (padicNorm p) → Prop) r 0
⊢ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔ Eq (α := ℚ_[p]) ⟦r⟧ 0

Tactic:
erw [Padic.zero_def, Quotient.eq]

Premises used: Padic.zero_def, Quotient.eq
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔
    (equiv : CauSeq ℚ (padicNorm p) → CauSeq ℚ (padicNorm p) → Prop) r 0

Tactic:
PadicSeq.norm_zero_iff r

Premises used: PadicSeq.norm_zero_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦r⟧ = 0 ↔
    (equiv : CauSeq ℚ (padicNorm p) → CauSeq ℚ (padicNorm p) → Prop) r 0

Tactic:
exact PadicSeq.norm_zero_iff r

Premises used: PadicSeq.norm_zero_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
max₁ :
  Max.max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r) ≤
    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

Tactic:
trans
      max ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) q)
        ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) r)

Premises used: Max.max, Quotient.lift, PadicSeq.norm, PadicSeq.norm_equiv
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h :
  ∀ (a b : CauSeq ℚ (padicNorm p)),
    Quotient.lift PadicSeq.norm ⋯ (HAdd.hAdd (α := ℚ_[p]) ⟦a⟧ ⟦b⟧) ≤
      max (Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦a⟧) (Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦b⟧)
⊢ Quotient.lift PadicSeq.norm ⋯ (q + r) ≤ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r)

Tactic:
induction q, r using Quotient.inductionOn₂
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a b : CauSeq ℚ (padicNorm p)
⊢ Quotient.lift PadicSeq.norm ⋯ (HAdd.hAdd (α := ℚ_[p]) ⟦a⟧ ⟦b⟧) ≤
    max (Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦a⟧) (Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦b⟧)

Tactic:
apply PadicSeq.norm_nonarchimedean

Premises used: PadicSeq.norm_nonarchimedean
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
ha : 0 ≤ Quotient.lift PadicSeq.norm ⋯ q
hb : 0 ≤ Quotient.lift PadicSeq.norm ⋯ r
⊢ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r) ≤
    Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r

Tactic:
apply max_le_add_of_nonneg

Premises used: max_le_add_of_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
ha : ∀ (a : CauSeq ℚ (padicNorm p)), 0 ≤ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦a⟧
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ q

Tactic:
induction q using Quotient.inductionOn
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℚ_[p]
a : CauSeq ℚ (padicNorm p)
⊢ 0 ≤ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦a⟧

Tactic:
apply PadicSeq.norm_nonneg

Premises used: PadicSeq.norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
hb : ∀ (a : CauSeq ℚ (padicNorm p)), 0 ≤ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦a⟧
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ r

Tactic:
induction r using Quotient.inductionOn
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
a : CauSeq ℚ (padicNorm p)
⊢ 0 ≤ Quotient.lift (s := equiv) PadicSeq.norm ⋯ ⟦a⟧

Tactic:
apply PadicSeq.norm_nonneg

Premises used: PadicSeq.norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ (N : ℕ), ∀ i ≥ N, (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε
h :
  ∀ (N i : ℕ),
    i ≥ N →
      ∀ (N : (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε),
        Quotient.lift PadicSeq.norm ⋯ (HSub.hSub (α := ℚ_[p]) (Padic.mk f) (↑((↑f : ℕ → ℚ) i) : ℚ_[p])) < ε
⊢ ∃ (N : ℕ),
    ∀ i ≥ N, Quotient.lift PadicSeq.norm ⋯ (HSub.hSub (α := ℚ_[p]) (Padic.mk f) (↑((↑f : ℕ → ℚ) i) : ℚ_[p])) < ε

Tactic:
peel hyp with N
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
hyp : ∃ (N : ℕ), ∀ i ≥ N, (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε
N_1 i : ℕ
h : i ≥ N_1
N : (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε
⊢ Quotient.lift PadicSeq.norm ⋯ (HSub.hSub (α := ℚ_[p]) (Padic.mk f) (↑((↑f : ℕ → ℚ) i) : ℚ_[p])) < ε

Tactic:
use N
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
by_contra! : ∀ (h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm), False
⊢ ∃ (N : ℕ), ∀ i ≥ N, (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm < ε

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i ≥ N, ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm
obtain : ∀ (N : ℕ) (hN : ∀ j ≥ N, ∀ k ≥ N, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := cauchy₂ f hε

Premises used: CauSeq.cauchy₂
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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) < ε
rcases : ∀ (i : ℕ) (hi : i ≥ N) (hge : ε ≤ (f - const (padicNorm p) ((↑f : ℕ → ℚ) i)).norm), False
⊢ False

Tactic:
rcases h N with ⟨i, hi, hge⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ ε ≤ 0

Tactic:
rw [PadicSeq.norm, dif_pos h] at hge

Premises used: dif_pos, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
hge₁ : ε ≤ 0
⊢ f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0

Tactic:
rw [PadicSeq.norm, dif_pos h] at hge

Premises used: dif_pos, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 : ε ≤ 0
h : f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
⊢ False

Tactic:
not_lt_of_ge hge hε

Premises used: not_lt_of_ge
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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 : ε ≤ 0
h : f - const (padicNorm p) ((↑f : ℕ → ℚ) i) ≈ 0
⊢ False

Tactic:
exact not_lt_of_ge hge hε

Premises used: not_lt_of_ge
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ ¬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ε
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ ε ≤ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))

Tactic:
split_ifs at hge
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
apply : padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε
⊢ False

Tactic:
apply not_le_of_gt _ hge

Premises used: not_le_of_gt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
hgen : N ≤ stationaryPoint hne
⊢ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε

Tactic:
hN _ hgen _ hi
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
hgen : N ≤ stationaryPoint hne
⊢ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε

Tactic:
exact hN _ hgen _ hi
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)) : ℕ → ℚ) N) =
    padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne))

Tactic:
have := stationaryPoint_spec hne le_rfl hngen
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
inr : padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) N) < ε
⊢ padicNorm p ((↑(f - const (padicNorm p) ((↑f : ℕ → ℚ) i)) : ℕ → ℚ) (stationaryPoint hne)) < ε

Tactic:
rw [← this]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)) : ℕ → ℚ) N) < ε

Tactic:
hN _ le_rfl _ hi

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)) : ℕ → ℚ) N) < ε

Tactic:
exact hN _ le_rfl _ hi

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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))
⊢ 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

Premises used: le_rfl, PadicSeq.stationaryPoint, le_total
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ LE.le (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (q + r) : ℚ)
    (max ((padicNormE : (a : ℚ_[p]) → ℚ) q) ((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℚ)

Tactic:
Quotient.inductionOn₂ q r <| norm_nonarchimedean

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ Ne (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) q : ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) r : ℚ) →
    Eq (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (q + r) : ℚ)
      (max ((padicNormE : (a : ℚ_[p]) → ℚ) q) ((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℚ)

Tactic:
Quotient.inductionOn₂ q r fun _ _ ↦ PadicSeq.add_eq_max_of_ne

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p]) = padicNorm p q

Tactic:
norm_const _

Premises used: dite, PadicSeq.norm_const, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ q ≠ 0 → ∃ (n : ℤ), (padicNormE : (a : ℚ_[p]) → ℚ) q = HPow.hPow (α := ℚ) (↑p : ℚ) (-n)

Tactic:
Quotient.inductionOn q fun f hf ↦
    have : ¬f ≈ 0 := (ne_zero_iff_nequiv_zero f).1 hf
    norm_values_discrete f this

Premises used: Quotient.inductionOn
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
inl : ∀ (heq : q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
inr : ∀ (hne' : ¬q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0), (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε
⊢ (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε

Tactic:
rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'

Premises used: HSub.hSub, Decidable.em, HasEquiv.Equiv, CauSeq.const, padicNorm, OfNat.ofNat, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p ((↑q' : ℕ → ℚ) m - (↑q' : ℕ → ℚ) n) < ε
heq : q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N) ≈ 0
⊢ (q' - const (padicNorm p) ((↑q' : ℕ → ℚ) N)).norm < ε

Tactic:
simpa only [heq, PadicSeq.norm, dif_pos]

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

Tactic:
simp only [PadicSeq.norm, dif_neg hne']

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

Tactic:
change padicNorm p (q' _ - q' _) < ε

Premises used: HSub.hSub, padicNorm, Subtype.val