awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y x : ℤ_[p]
hx : x ≠ 0
rw : (↑(unitCoeff hx) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) x.valuation = x
rw₁ rw₂ : x = x
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) x.valuation * (↑(unitCoeff hx) : ℤ_[p]) = x

Tactic:
rw [mul_comm, ← unitCoeff_spec hx]

Premises used: mul_comm, PadicInt.unitCoeff_spec
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
s : Ideal ℤ_[p]
hs : s ≠ ⊥
⊢ ∃ (n : ℕ), s = Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}

Tactic:
IsDiscreteValuationRing.ideal_eq_span_pow_irreducible hs irreducible_p

Premises used: PadicInt.irreducible_p, IsDiscreteValuationRing.ideal_eq_span_pow_irreducible
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx :
  ∀ {m n : ℕ},
    m ≤ n →
      x m ≡ x n [SMOD HSMul.hSMul (β := Submodule ℤ_[p] ℤ_[p]) (HPow.hPow (α := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) m) ⊤]
simp :
  ∀ (hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))),
    ∃ (L : ℤ_[p]), ∀ (n : ℕ), ‖x n - L‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ∃ (L : ℤ_[p]),
    ∀ (n : ℕ),
      x n ≡ L [SMOD HSMul.hSMul (β := Submodule ℤ_[p] ℤ_[p]) (HPow.hPow (α := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) n) ⊤]

Tactic:
simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.sub_mem, maximalIdeal_eq_span_p,
      Ideal.span_singleton_pow, ← norm_le_pow_iff_mem_span_pow] at hx ⊢

Premises used: Ideal.one_eq_top, PadicInt.maximalIdeal_eq_span_p, SModEq.sub_mem, PadicInt.norm_le_pow_iff_mem_span_pow, smul_eq_mul, mul_one, Ideal.span_singleton_pow
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
refine_2 : ∃ (L : ℤ_[p]), ∀ (n : ℕ), ‖x n - L‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
refine_1 : IsCauSeq norm x
⊢ ∃ (L : ℤ_[p]), ∀ (n : ℕ), ‖x n - L‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
let x' : CauSeq ℤ_[p] norm := ⟨x, ?_⟩
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
ε : ℝ
hε : ε > 0
refine_1 : ∀ (m : ℕ) (hm : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ)) < ε), ∃ (i : ℕ), ∀ j ≥ i, ‖x j - x i‖ < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖x j - x i‖ < ε

Tactic:
obtain ⟨m, hm⟩ := exists_pow_neg_lt p hε

Premises used: PadicInt.exists_pow_neg_lt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
ε : ℝ
hε : ε > 0
m : ℕ
hm : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ)) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖x j - x i‖ < ε

Tactic:
⟨m, fun n hn => lt_of_le_of_lt ?_ hm⟩

Premises used: lt_of_le_of_lt, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
ε : ℝ
hε : ε > 0
m : ℕ
hm : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ)) < ε
refine_1 : ∀ (n : ℕ) (hn : n ≥ m), ‖x n - x m‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖x j - x i‖ < ε

Tactic:
refine ⟨m, fun n hn => lt_of_le_of_lt ?_ hm⟩
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
ε : ℝ
hε : ε > 0
m : ℕ
hm : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ)) < ε
n : ℕ
hn : n ≥ m
refine_1 : ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
⊢ ‖x n - x m‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))

Tactic:
rw [← neg_sub, norm_neg]

Premises used: neg_sub, norm_neg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
ε : ℝ
hε : ε > 0
m : ℕ
hm : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ)) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))

Tactic:
hx hn
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
ε : ℝ
hε : ε > 0
m : ℕ
hm : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ)) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))

Tactic:
exact hx hn
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
⊢ ∃ (L : ℤ_[p]), ∀ (n : ℕ), ‖x n - L‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
⟨x'.lim, fun n => ?_⟩

Premises used: CauSeq.lim, Exists.intro
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
refine_2 : ∀ (n : ℕ), ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ∃ (L : ℤ_[p]), ∀ (n : ℕ), ‖x n - L‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
refine ⟨x'.lim, fun n => ?_⟩
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := zpow_pos (mod_cast hp.out.pos) _
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
refine_2 :
  ∀ (i : ℕ)
    (hi :
      ∀ j ≥ i,
        ∀ k ≥ j,
          ‖(↑x' : ℕ → ℤ_[p]) k - (↑(const norm x'.lim) : ℕ → ℤ_[p]) j‖ <
            HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))),
    ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this

Premises used: CauSeq.equiv_lim, CauSeq.equiv_def₃
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hi :
  ∀ j ≥ i,
    ∀ k ≥ j,
      ‖(↑x' : ℕ → ℤ_[p]) k - (↑(const norm x'.lim) : ℕ → ℤ_[p]) j‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
pos : ∀ (hin : i ≤ n), ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
neg : ∀ (hin : n < i), ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
by_cases! hin : i ≤ n
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hi :
  ∀ j ≥ i,
    ∀ k ≥ j,
      ‖(↑x' : ℕ → ℤ_[p]) k - (↑(const norm x'.lim) : ℕ → ℤ_[p]) j‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hin : i ≤ n
⊢ ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
(hi i le_rfl n hin).le

Premises used: le_rfl, LT.lt.le, CauSeq.lim, Classical.choose
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hi :
  ∀ j ≥ i,
    ∀ k ≥ j,
      ‖(↑x' : ℕ → ℤ_[p]) k - (↑(const norm x'.lim) : ℕ → ℤ_[p]) j‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hin : i ≤ n
⊢ ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
exact (hi i le_rfl n hin).le

Premises used: le_rfl, LT.lt.le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hi :
  ∀ j ≥ i,
    ∀ k ≥ j,
      ‖(↑x' : ℕ → ℤ_[p]) k - (↑(const norm x'.lim) : ℕ → ℤ_[p]) j‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hin : n < i
⊢ ‖(↑x' : ℕ → ℤ_[p]) i - (↑(const norm x'.lim) : ℕ → ℤ_[p]) i‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
specialize hi i le_rfl i le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hin : n < i
hi : ‖(↑x' : ℕ → ℤ_[p]) i - (↑(const norm x'.lim) : ℕ → ℤ_[p]) i‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖x n - x i‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
specialize hx hin.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx_1 : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hin : n < i
hi : ‖(↑x' : ℕ → ℤ_[p]) i - (↑(const norm x'.lim) : ℕ → ℤ_[p]) i‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hx : ‖x n - x i‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖x n - x i + (x i - x'.lim)‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖

Tactic:
have := nonarchimedean (x n - x i : ℤ_[p]) (x i - x'.lim)
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx_1 : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this_1 : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hin : n < i
hi : ‖(↑x' : ℕ → ℤ_[p]) i - (↑(const norm x'.lim) : ℕ → ℤ_[p]) i‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hx : ‖x n - x i‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this : ‖x n - x i + (x i - x'.lim)‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖

Tactic:
rw [sub_add_sub_cancel] at this

Premises used: sub_add_sub_cancel
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx_1 : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this_1 : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hin : n < i
hi : ‖(↑x' : ℕ → ℤ_[p]) i - (↑(const norm x'.lim) : ℕ → ℤ_[p]) i‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hx : ‖x n - x i‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this : ‖x n - x'.lim‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

Premises used: Iff.mpr, LT.lt.le, max_le_iff, And.intro, LE.le.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℕ → ℤ_[p]
hx_1 : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑m : ℤ))
x' : CauSeq ℤ_[p] norm := Subtype.mk (p := fun (f : ℕ → ℤ_[p]) ↦ IsCauSeq norm f) x ⋯
n : ℕ
this_1 : 0 < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
i : ℕ
hin : n < i
hi : ‖(↑x' : ℕ → ℤ_[p]) i - (↑(const norm x'.lim) : ℕ → ℤ_[p]) i‖ < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
hx : ‖x n - x i‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this : ‖x n - x'.lim‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
exact this.trans (max_le_iff.mpr ⟨hx, hi.le⟩)

Premises used: Iff.mpr, LT.lt.le, max_le_iff, And.intro, LE.le.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x = (↑x : ℚ_[p])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x_2 : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x
rwa :
  IsUnit
    (↑(↑(Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x) x hx) :
          ℤ_[p]) :
      ℚ_[p])
rwa₁ :
  (↑(↑(Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x) x hx) :
          ℤ_[p]) :
      ℚ_[p]) ≠
    0
rwa₂ :
  (↑(Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x) x hx) :
      ℤ_[p]) ≠
    0
rwa₃ rwa₄ rwa₅ rwa₆ :
  Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p])
    (↑(Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x) x hx) :
      ℤ_[p])
⊢ IsUnit (M := ℚ_[p])
    ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
        (↑(Subtype.mk (p := fun (x : ℤ_[p]) ↦ Membership.mem (γ := Submonoid ℤ_[p]) (nonZeroDivisors ℤ_[p]) x) x hx) :
          ℤ_[p]) :
      ℚ_[p])

Tactic:
rwa [algebraMap_apply, isUnit_iff_ne_zero, PadicInt.coe_ne_zero, ←
      mem_nonZeroDivisors_iff_ne_zero]

Premises used: PadicInt.coe_ne_zero, PadicInt.algebraMap_apply, isUnit_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
pos :
  ∀ (hx : ‖x‖ ≤ 1),
    ∃ (x_2 : ℤ_[p] × ↥(nonZeroDivisors ℤ_[p])),
      HMul.hMul (β := ℚ_[p]) x ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (↑x_2.2 : ℤ_[p]) : ℚ_[p]) =
        (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x_2.1
neg :
  ∀ (hx : ¬‖x‖ ≤ 1),
    ∃ (x_2 : ℤ_[p] × ↥(nonZeroDivisors ℤ_[p])),
      HMul.hMul (β := ℚ_[p]) x ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (↑x_2.2 : ℤ_[p]) : ℚ_[p]) =
        (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x_2.1
⊢ ∃ (x_2 : ℤ_[p] × ↥(nonZeroDivisors ℤ_[p])),
    HMul.hMul (β := ℚ_[p]) x ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (↑x_2.2 : ℤ_[p]) : ℚ_[p]) =
      (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x_2.1

Tactic:
by_cases hx : ‖x‖ ≤ 1
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
h :
  x *
      (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
        (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).2 : ℤ_[p]) =
    (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).1
⊢ ∃ (x_2 : ℤ_[p] × ↥(nonZeroDivisors ℤ_[p])),
    HMul.hMul (β := ℚ_[p]) x ((algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (↑x_2.2 : ℤ_[p]) : ℚ_[p]) =
      (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) x_2.1

Tactic:
use (⟨x, hx⟩, 1)

Premises used: Prod.mk, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ‖x‖ ≤ 1
h :
  x * (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) 1 =
    (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).1
h₁ : x * 1 = (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).1
h₂ : x = (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).1
h₃ : x = (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).1 : ℚ_[p])
h₄ h₅ : x = x
⊢ x *
      (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p])
        (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).2 : ℤ_[p]) =
    (algebraMap ℤ_[p] ℚ_[p] : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) x hx, 1).1

Tactic:
rw [Submonoid.coe_one, map_one, mul_one, PadicInt.algebraMap_apply, Subtype.coe_mk]

Premises used: Subtype.coe_mk, PadicInt.algebraMap_apply, Submonoid.coe_one, map_one, mul_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
⊢ let n := (-x.valuation).toNat;
  n = (-x.valuation).toNat

Tactic:
set n := Int.toNat (-x.valuation) with hn

Premises used: Padic.valuation, Int.toNat, Neg.neg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
rw : 0 ≤ -x.valuation
⊢ (↑n : ℤ) = -x.valuation

Tactic:
rw [hn, Int.toNat_of_nonneg]

Premises used: Int.toNat_of_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
rw : x.valuation ≤ 0
⊢ 0 ≤ -x.valuation

Tactic:
rw [Right.nonneg_neg_iff]

Premises used: Right.nonneg_neg_iff
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation < 0

Tactic:
rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx

Premises used: not_le, Padic.norm_le_one_iff_val_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hx₁ : x.valuation < 0
⊢ let n := (-x.valuation).toNat;
  n = (-x.valuation).toNat

Tactic:
rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx

Premises used: not_le, Padic.norm_le_one_iff_val_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : x.valuation < 0
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0

Tactic:
hx.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : x.valuation < 0
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ x.valuation ≤ 0

Tactic:
exact hx.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
⊢ (↑n : ℤ) = -x.valuation

Tactic:
have hn_coe : (n : ℤ) = -x.valuation := by
        rw [hn, Int.toNat_of_nonneg]
        rw [Right.nonneg_neg_iff]
        rw [Padic.norm_le_one_iff_val_nonneg, not_le] at hx
        exact hx.le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
⊢ let a := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n;
  a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n

Tactic:
set a := x * (p : ℚ_[p]) ^ n with ha

Premises used: Nat.cast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
⊢ ¬LE.le (α := ℝ) 0 1

Tactic:
rw [h0, norm_zero] at hx

Premises used: norm_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
hx₁ : ¬LE.le (α := ℝ) 0 1
⊢ let n := (-x.valuation).toNat;
  n = (-x.valuation).toNat

Tactic:
rw [h0, norm_zero] at hx

Premises used: norm_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
hx₁ : ¬LE.le (α := ℝ) 0 1
hn₁ :
  let n := (-x.valuation).toNat;
  n = (-x.valuation).toNat
⊢ let n := (-x.valuation).toNat;
  (↑n : ℤ) = -x.valuation

Tactic:
rw [h0, norm_zero] at hx

Premises used: norm_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
hx₁ : ¬LE.le (α := ℝ) 0 1
hn₁ :
  let n := (-x.valuation).toNat;
  n = (-x.valuation).toNat
hn_coe₁ :
  let n := (-x.valuation).toNat;
  (↑n : ℤ) = -x.valuation
⊢ let n := (-x.valuation).toNat;
  let a := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n;
  a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n

Tactic:
rw [h0, norm_zero] at hx

Premises used: norm_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
hx₁ : ¬LE.le (α := ℝ) 0 1
hn₁ :
  let n := (-x.valuation).toNat;
  n = (-x.valuation).toNat
hn_coe₁ :
  let n := (-x.valuation).toNat;
  (↑n : ℤ) = -x.valuation
ha₁ :
  let n := (-x.valuation).toNat;
  let a := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n;
  a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
⊢ x = 0

Tactic:
rw [h0, norm_zero] at hx

Premises used: norm_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬LE.le (α := ℝ) 0 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
⊢ False

Tactic:
hx zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y : ℤ_[p]
x : ℚ_[p]
hx : ¬LE.le (α := ℝ) 0 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : (↑n : ℤ) = -x.valuation
a : ℚ_[p] := x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
ha : a = x * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n
h0 : x = 0
⊢ False

Tactic:
exact hx zero_le_one

Premises used: zero_le_one