awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
coe :
  ∀ (hx : 0 ≤ x),
    ∃ (a : ℚ),
      Eq (α := WithZero (Multiplicative ℤ))
        (({
                toFun := fun (x : ℚ) ↦
                  if x = 0 then 0
                  else
                    (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                      WithZero (Multiplicative ℤ)),
                map_zero' := ⋯ } :
              (a : ℚ) → WithZero (Multiplicative ℤ))
            a :
          WithZero (Multiplicative ℤ))
        ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
          WithZero (Multiplicative ℤ))
coe₁ :
  ∀ (hx : x < 0),
    ∃ (a : ℚ),
      Eq (α := WithZero (Multiplicative ℤ))
        (({
                toFun := fun (x : ℚ) ↦
                  if x = 0 then 0
                  else
                    (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                      WithZero (Multiplicative ℤ)),
                map_zero' := ⋯ } :
              (a : ℚ) → WithZero (Multiplicative ℤ))
            a :
          WithZero (Multiplicative ℤ))
        ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
          WithZero (Multiplicative ℤ))
⊢ ∃ (a : ℚ),
    Eq (α := WithZero (Multiplicative ℤ))
      (({
              toFun := fun (x : ℚ) ↦
                if x = 0 then 0
                else
                  (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                    WithZero (Multiplicative ℤ)),
              map_zero' := ⋯ } :
            (a : ℚ) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))

Tactic:
rcases le_or_gt 0 x with (hx | hx)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : 0 ≤ x
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (({
            toFun := fun (x : ℚ) ↦
              if x = 0 then 0
              else
                (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                  WithZero (Multiplicative ℤ)),
            map_zero' := ⋯ } :
          (a : ℚ) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := ℚ) (↑p : ℚ) x.natAbs)⁻¹ :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
simp [hp.out.ne_zero, hx]

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : 0 ≤ x
⊢ ∃ (a : ℚ),
    Eq (α := WithZero (Multiplicative ℤ))
      (({
              toFun := fun (x : ℚ) ↦
                if x = 0 then 0
                else
                  (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                    WithZero (Multiplicative ℤ)),
              map_zero' := ⋯ } :
            (a : ℚ) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))

Tactic:
exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : x < 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (({
            toFun := fun (x : ℚ) ↦
              if x = 0 then 0
              else
                (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                  WithZero (Multiplicative ℤ)),
            map_zero' := ⋯ } :
          (a : ℚ) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := ℚ) (↑p : ℚ) x.natAbs) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]

Premises used: Iff.mpr, LT.lt.le, abs_eq_neg_self, Nat.Prime.ne_zero, padicValRat.pow, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
hx : x < 0
⊢ ∃ (a : ℚ),
    Eq (α := WithZero (Multiplicative ℤ))
      (({
              toFun := fun (x : ℚ) ↦
                if x = 0 then 0
                else
                  (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-padicValRat p x)) :
                    WithZero (Multiplicative ℤ)),
              map_zero' := ⋯ } :
            (a : ℚ) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))

Tactic:
exact ⟨p ^ x.natAbs, by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : WithZero (Multiplicative ℤ)
zero :
  ∃ (a : ℚ),
    Eq (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
coe :
  ∀ (x : Multiplicative ℤ),
    ∃ (a : ℚ), (padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a = (↑x : WithZero (Multiplicative ℤ))
⊢ ∃ (a : ℚ), (padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a = x

Tactic:
induction x with
  | zero => simp
  | coe x =>
    induction x with | ofAdd x
    simp_rw [Rat.padicValuation, WithZero.exp, Valuation.coe_mk, MonoidWithZeroHom.coe_mk]
    rcases le_or_gt 0 x with (hx | hx)
    · exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩
    · exact ⟨p ^ x.natAbs, by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]⟩

Premises used: MonoidWithZeroHom.coe_mk, le_or_gt, WithZero.coe, WithZero.exp, Rat.padicValuation, Valuation.coe_mk, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
⊢ padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε

Tactic:
have : padicNorm p (f n - f m) < ε := hN2 _ (max_le_iff.1 hn).2 _ (max_le_iff.1 hm).2
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
⊢ padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)

Tactic:
have : padicNorm p (f n - f m) < padicNorm p (f n) :=
      lt_of_lt_of_le this <| hN1 _ (max_le_iff.1 hn).1
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
⊢ padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))

Tactic:
have : padicNorm p (f n - f m) < max (padicNorm p (f n)) (padicNorm p (f m)) :=
      lt_max_iff.2 (Or.inl this)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
by_contra : ∀ (hne : ¬padicNorm p ((↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)), False
⊢ padicNorm p ((↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)

Tactic:
by_contra hne
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
hne : ¬padicNorm p ((↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
⊢ ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)

Tactic:
rw [← padicNorm.neg (f m)] at hne

Premises used: padicNorm.neg, Subtype.val
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
hne : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
⊢ padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p (-(↑f : ℕ → ℚ) m)) (padicNorm p ((↑f : ℕ → ℚ) n))

Tactic:
have hnam := add_eq_max_of_ne hne
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
hne : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
hnam :
  padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p (-(↑f : ℕ → ℚ) m)) (padicNorm p ((↑f : ℕ → ℚ) n))
⊢ padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))

Tactic:
rw [padicNorm.neg, max_comm] at hnam

Premises used: padicNorm.neg, max_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
hne : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
hnam :
  padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
⊢ padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) < padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n)

Tactic:
rw [← hnam, sub_eq_add_neg, add_comm] at this

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
hne : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
hnam :
  padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
this₁ : padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) < padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n)
⊢ ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)

Tactic:
rw [← hnam, sub_eq_add_neg, add_comm] at this

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
hne : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
hnam :
  padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
this₁ : padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) < padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n)
hne₁ : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
⊢ padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))

Tactic:
rw [← hnam, sub_eq_add_neg, add_comm] at this

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this_1 : ∃ ε > 0, ∃ (N1 : ℕ), ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, ε ≤ padicNorm p ((↑f : ℕ → ℚ) j)
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNorm p ((↑f : ℕ → ℚ) j - (↑f : ℕ → ℚ) k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this_2 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < ε
this_3 : padicNorm p ((↑f : ℕ → ℚ) n - (↑f : ℕ → ℚ) m) < padicNorm p ((↑f : ℕ → ℚ) n)
this : padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) < padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n)
hne : ¬padicNorm p (-(↑f : ℕ → ℚ) m) = padicNorm p ((↑f : ℕ → ℚ) n)
hnam :
  padicNorm p (-(↑f : ℕ → ℚ) m + (↑f : ℕ → ℚ) n) = max (padicNorm p ((↑f : ℕ → ℚ) n)) (padicNorm p ((↑f : ℕ → ℚ) m))
⊢ False

Tactic:
apply _root_.lt_irrefl _ this

Premises used: lt_irrefl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ∀ {m n : ℕ},
    stationaryPoint hf ≤ m → stationaryPoint hf ≤ n → padicNorm p ((↑f : ℕ → ℚ) n) = padicNorm p ((↑f : ℕ → ℚ) m)

Tactic:
@(Classical.choose_spec <| stationary hf)

Premises used: PadicSeq.stationaryPoint, Classical.choose_spec, PadicSeq.stationary
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
mp : f.norm = 0 → f ≈ 0
mpr : f ≈ 0 → f.norm = 0
⊢ f.norm = 0 ↔ f ≈ 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
h : f.norm = 0
mp : ∀ (hf : ¬f ≈ 0), False
⊢ f ≈ 0

Tactic:
by_contra hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
h : Eq (α := ℚ) (if hf : f ≈ 0 then 0 else padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))) 0
hf : ¬f ≈ 0
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = 0

Tactic:
split_ifs at h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = 0
mp : f ≈ 0
⊢ False

Tactic:
apply hf
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
mp : ∀ j ≥ stationaryPoint hf, padicNorm p ((↑(f - 0) : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p ((↑(f - 0) : ℕ → ℚ) j) < ε

Tactic:
exists stationaryPoint hf

Premises used: PadicSeq.stationaryPoint
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
⊢ padicNorm p ((↑f : ℕ → ℚ) j) = padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))

Tactic:
have heq := stationaryPoint_spec hf le_rfl hj
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
heq : padicNorm p ((↑f : ℕ → ℚ) j) = padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
⊢ padicNorm p ((↑(f - 0) : ℕ → ℚ) j) < ε

Tactic:
simpa [h, heq]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ f.norm = 0

Tactic:
simp [norm, h]

Premises used: PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p ((↑f : ℕ → ℚ) k) = padicNorm p ((↑g : ℕ → ℚ) k)
hf : f ≈ 0
ε : ℚ
hε : ε > 0
i : ℕ
hi : ∀ j ≥ i, padicNorm p ((↑(f - 0) : ℕ → ℚ) j) < ε
j : ℕ
hj : j ≥ i
⊢ padicNorm p ((↑(g - 0) : ℕ → ℚ) j) < ε

Tactic:
simpa [h] using hi _ hj
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm ≠ 0

Tactic:
hf ∘ f.norm_zero_iff.1

Premises used: Function.comp, Iff.mp, PadicSeq.norm_zero_iff, Not
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))

Tactic:
simp [norm, hf]

Premises used: PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
heq : f.norm = padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf))
h : (↑f : ℕ → ℚ) (stationaryPoint hf) = 0
⊢ f.norm = 0

Tactic:
simpa [h] using heq
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ ¬LimZero (const (padicNorm p) q)

Tactic:
fun h' ↦ hq <| const_limZero.1 h'

Premises used: CauSeq.const_limZero, Iff.mp, Not
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
h : (HSub.hSub (α := CauSeq ℚ (padicNorm p)) (const (padicNorm p) q) 0).LimZero
⊢ LimZero (const (padicNorm p) q)

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
simp [hf, norm]

Premises used: PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
simp [norm, hf, padicNorm.nonneg]

Premises used: padicNorm.nonneg, PadicSeq.norm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
exact if hf : f ≈ 0 then by simp [hf, norm] else by simp [norm, hf, padicNorm.nonneg]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
classical exact if hf : f ≈ 0 then by simp [hf, norm] else by simp [norm, hf, padicNorm.nonneg]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
a : stationaryPoint hf ≤ max (stationaryPoint hf) (max v2 v3)
a₁ : stationaryPoint hf ≤ stationaryPoint hf
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) (max (stationaryPoint hf) (max v2 v3)))

Tactic:
apply stationaryPoint_spec hf

Premises used: PadicSeq.stationaryPoint_spec
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ max (stationaryPoint hf) (max v2 v3)

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
a : stationaryPoint hf ≤ max v1 (max (stationaryPoint hf) v3)
a₁ : stationaryPoint hf ≤ stationaryPoint hf
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) (max v1 (max (stationaryPoint hf) v3)))

Tactic:
apply stationaryPoint_spec hf

Premises used: PadicSeq.stationaryPoint_spec
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
a : stationaryPoint hf ≤ max (stationaryPoint hf) v3
a₁ : max (stationaryPoint hf) v3 ≤ max v1 (max (stationaryPoint hf) v3)
a₂ : ℕ
⊢ stationaryPoint hf ≤ max v1 (max (stationaryPoint hf) v3)

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ max (stationaryPoint hf) v3

Tactic:
apply le_max_left _ v3

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ max (stationaryPoint hf) v3 ≤ max v1 (max (stationaryPoint hf) v3)

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
a : stationaryPoint hf ≤ max v1 (max v2 (stationaryPoint hf))
a₁ : stationaryPoint hf ≤ stationaryPoint hf
⊢ padicNorm p ((↑f : ℕ → ℚ) (stationaryPoint hf)) = padicNorm p ((↑f : ℕ → ℚ) (max v1 (max v2 (stationaryPoint hf))))

Tactic:
apply stationaryPoint_spec hf

Premises used: PadicSeq.stationaryPoint_spec