awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ max ‖z1‖ ‖z2‖

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖(↑z : ℚ_[p])‖ = ‖z‖

Tactic:
simp [norm_def]

Premises used: PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ norm (E := ℤ_[p]) (↑z : ℤ_[p]) = norm (E := ℚ_[p]) (↑z : ℚ_[p])

Tactic:
simp [norm_def]

Premises used: PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
hq : ‖q‖ ≤ 1
⊢ norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) q hq) = ‖q‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (E := ℤ_[p]) (↑p : ℤ_[p]) = (↑p : ℝ)⁻¹

Tactic:
Padic.norm_p

Premises used: Padic.norm_p
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n‖ = HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ 1 ≤ ‖x‖ ↔ ‖x‖ = 1

Tactic:
simp [le_antisymm_iff, ← padic_norm_e_of_padicInt, x.prop]

Premises used: PadicInt.padic_norm_e_of_padicInt, le_antisymm_iff, Subtype.prop
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (E := ℤ_[p]) (↑(p - 1) : ℤ_[p]) = 1

Tactic:
simp [norm_def]

Premises used: PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
f : CauSeq ℤ_[p] norm
x_1 : ℝ
hε : x_1 > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      (fun (a : ℚ_[p]) ↦ ‖a‖)
          (HSub.hSub (α := ℚ_[p]) ((fun (n : ℕ) ↦ (↑((↑f : ℕ → ℤ_[p]) n) : ℚ_[p])) j)
            ((fun (n : ℕ) ↦ (↑((↑f : ℕ → ℤ_[p]) n) : ℚ_[p])) i)) <
        x_1

Tactic:
simpa [norm, norm_def] using f.cauchy hε

Premises used: Norm.norm, CauSeq.cauchy, PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
f : CauSeq ℤ_[p] norm
hqn : ‖(cauSeq_to_rat_cauSeq f).lim‖ ≤ 1
ε : ℝ
⊢ ε > 0 →
    ∃ (i : ℕ),
      ∀ j ≥ i,
        ‖(↑(f - CauSeq.const norm (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (cauSeq_to_rat_cauSeq f).lim hqn)) :
                ℕ → ℤ_[p])
              j‖ <
          ε

Tactic:
simpa [norm, norm_def] using CauSeq.equiv_lim (cauSeq_to_rat_cauSeq f) ε

Premises used: Norm.norm, _private.0.PadicInt.cauSeq_to_rat_cauSeq, CauSeq.equiv_lim, PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
obtain : ∀ (k : ℕ) (hk : ε⁻¹ < (↑k : ℝ)), ∃ (k : ℕ), HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
⊢ ∃ (k : ℕ), HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε

Tactic:
obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹

Premises used: Inv.inv, exists_nat_gt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
⊢ ∃ (k : ℕ), HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε

Tactic:
use k
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : ε⁻¹ < (HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)))⁻¹
rw : LT.lt (α := ℝ) 0 (↑p : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε

Tactic:
rw [← inv_lt_inv₀ hε (zpow_pos _ _)]

Premises used: zpow_pos, inv_lt_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : ε⁻¹ < HPow.hPow (α := ℝ) (↑p : ℝ) k
⊢ ε⁻¹ < (HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)))⁻¹

Tactic:
rw [zpow_neg, inv_inv, zpow_natCast]

Premises used: zpow_natCast, inv_inv, zpow_neg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : (↑k : ℝ) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) k
⊢ ε⁻¹ < HPow.hPow (α := ℝ) (↑p : ℝ) k

Tactic:
apply lt_of_lt_of_le hk

Premises used: lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : k ≤ p ^ k
⊢ (↑k : ℝ) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) k

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : k < p ^ k
⊢ k ≤ p ^ k

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
⊢ k < p ^ k

Tactic:
Nat.lt_pow_self _

Premises used: Nat.lt_pow_self
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
h : 1 < p
⊢ k < p ^ k

Tactic:
convert! Nat.lt_pow_self _ using 1

Premises used: Nat.lt_pow_self
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
⊢ 1 < p

Tactic:
hp.1.one_lt

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
⊢ 1 < p

Tactic:
exact hp.1.one_lt

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑p : ℝ)

Tactic:
mod_cast hp.1.pos

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.Prime.pos, Nat.cast, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < (↑k : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑p : ℝ)

Tactic:
exact mod_cast hp.1.pos

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
obtain :
  ∀ (k : ℕ) (hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)),
    ∃ (k : ℕ), HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
⊢ ∃ (k : ℕ), HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε

Tactic:
obtain ⟨k, hk⟩ := @exists_pow_neg_lt p _ ε (mod_cast hε)

Premises used: congrArg, cast, Rat.natCast_lt_cast._simp_1, Rat.cast, LT.lt, PadicInt.exists_pow_neg_lt, congrFun', Nat.cast_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)
h : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
⊢ ∃ (k : ℕ), HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε

Tactic:
use k
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)
⊢ Eq (α := ℝ) (↑p : ℝ) (↑(↑p : ℚ) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)

Tactic:
rw [show (p : ℝ) = (p : ℚ) by simp] at hk
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)
⊢ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε

Tactic:
mod_cast hk

Premises used: congrArg, cast, Rat.cast, Nat.cast, LT.lt, congrFun', Rat.cast_lt._simp_1, Rat.cast_zpow._simp_1, Neg.neg, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑k : ℤ)) < (↑ε : ℝ)
⊢ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε

Tactic:
exact mod_cast hk
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
this rwa rwa₁ rwa₂ rwa₃ : norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 ↔ (↑p : ℤ) ∣ k
⊢ norm (E := ℤ_[p]) (↑k : ℤ_[p]) < 1 ↔ (↑p : ℤ) ∣ k

Tactic:
rwa [norm_intCast_eq_padic_norm]

Premises used: PadicInt.norm_intCast_eq_padic_norm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this :
  norm (E := ℚ_[p]) (↑k : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k
⊢ norm (E := ℤ_[p]) (↑k : ℤ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k

Tactic:
simpa [norm_intCast_eq_padic_norm]

Premises used: PadicInt.norm_intCast_eq_padic_norm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : norm (E := ℚ_[p]) (↑(↑n : ℤ_[p]) : ℚ_[p]) = 1 ↔ p.Coprime n
rw₁ : norm (E := ℚ_[p]) (↑n : ℚ_[p]) = 1 ↔ p.Coprime n
rw₂ rw₃ : p.Coprime n ↔ p.Coprime n
⊢ norm (E := ℤ_[p]) (↑n : ℤ_[p]) = 1 ↔ p.Coprime n

Tactic:
rw [norm_def, coe_natCast, Padic.norm_natCast_eq_one_iff]

Premises used: PadicInt.coe_natCast, Padic.norm_natCast_eq_one_iff, PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : norm (E := ℚ_[p]) (↑(↑n : ℤ_[p]) : ℚ_[p]) < 1 ↔ p ∣ n
rw₁ : norm (E := ℚ_[p]) (↑n : ℚ_[p]) < 1 ↔ p ∣ n
rw₂ rw₃ : p ∣ n ↔ p ∣ n
⊢ norm (E := ℤ_[p]) (↑n : ℤ_[p]) < 1 ↔ p ∣ n

Tactic:
rw [norm_def, coe_natCast, Padic.norm_natCast_lt_one_iff]

Premises used: Padic.norm_natCast_lt_one_iff, PadicInt.coe_natCast, PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
rw : norm (E := ℚ_[p]) (↑(↑z : ℤ_[p]) : ℚ_[p]) = 1 ↔ IsCoprime z (↑p : ℤ)
rw₁ : norm (E := ℚ_[p]) (↑z : ℚ_[p]) = 1 ↔ IsCoprime z (↑p : ℤ)
rw₂ rw₃ : IsCoprime z (↑p : ℤ) ↔ IsCoprime z (↑p : ℤ)
⊢ norm (E := ℤ_[p]) (↑z : ℤ_[p]) = 1 ↔ IsCoprime z (↑p : ℤ)

Tactic:
rw [norm_def, coe_intCast, Padic.norm_intCast_eq_one_iff]

Premises used: Padic.norm_intCast_eq_one_iff, PadicInt.norm_def, PadicInt.coe_intCast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
rw : norm (E := ℚ_[p]) (↑(↑z : ℤ_[p]) : ℚ_[p]) < 1 ↔ (↑p : ℤ) ∣ z
rw₁ : norm (E := ℚ_[p]) (↑z : ℚ_[p]) < 1 ↔ (↑p : ℤ) ∣ z
rw₂ rw₃ : (↑p : ℤ) ∣ z ↔ (↑p : ℤ) ∣ z
⊢ norm (E := ℤ_[p]) (↑z : ℤ_[p]) < 1 ↔ (↑p : ℤ) ∣ z

Tactic:
rw [norm_def, coe_intCast, Padic.norm_intCast_lt_one_iff]

Premises used: Padic.norm_intCast_lt_one_iff, PadicInt.norm_def, PadicInt.coe_intCast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
inl : 0 ≤ valuation (p := p) (↑0 : ℚ_[p])
inr : ∀ (hx : x ≠ 0), 0 ≤ (↑x : ℚ_[p]).valuation
⊢ 0 ≤ (↑x : ℚ_[p]).valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 0 ≤ valuation (p := p) (↑0 : ℚ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖(↑x : ℚ_[p])‖ ≤ 1

Tactic:
have := x.2
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : ‖(↑x : ℚ_[p])‖ ≤ 1
inr : ∀ (this : HPow.hPow (α := ℝ) (↑p : ℝ) (-(↑x : ℚ_[p]).valuation) ≤ 1), LT.lt (α := ℝ) 1 (↑p : ℝ)
⊢ 0 ≤ (↑x : ℚ_[p]).valuation

Tactic:
rwa [Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx, zpow_le_one_iff_right₀, neg_nonpos]
    at this

Premises used: Iff.mpr, PadicInt.coe_ne_zero, neg_nonpos, Padic.norm_eq_zpow_neg_valuation, zpow_le_one_iff_right₀
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : HPow.hPow (α := ℝ) (↑p : ℝ) (-(↑x : ℚ_[p]).valuation) ≤ 1
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
mod_cast hp.out.one_lt

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
this : HPow.hPow (α := ℝ) (↑p : ℝ) (-(↑x : ℚ_[p]).valuation) ≤ 1
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
exact mod_cast hp.out.one_lt

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x : ℚ_[p]).valuation = (↑x.valuation : ℤ)

Tactic:
simp [valuation, valuation_coe_nonneg]

Premises used: PadicInt.valuation_coe_nonneg, PadicInt.valuation
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) 0 = 0

Tactic:
simp [valuation]

Premises used: PadicInt.valuation
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) 1 = 0

Tactic:
simp [valuation]

Premises used: PadicInt.valuation
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation (p := p) (↑p : ℤ_[p]) = 1

Tactic:
simp [valuation]

Premises used: PadicInt.valuation
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
zify : LE.le (α := ℤ) (min (↑x.valuation : ℤ) (↑y.valuation : ℤ)) (↑(x + y).valuation : ℤ)
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
zify
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ LE.le (α := ℤ) (min (↑x.valuation : ℤ) (↑y.valuation : ℤ)) (↑(x + y).valuation : ℤ)

Tactic:
simpa [← valuation_coe] using Padic.le_valuation_add <| coe_ne_zero.2 hxy

Premises used: Iff.mpr, PadicInt.coe_ne_zero, Padic.le_valuation_add, PadicInt.valuation_coe
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
zify : (↑(x * y).valuation : ℤ) = HAdd.hAdd (α := ℤ) (↑x.valuation : ℤ) (↑y.valuation : ℤ)
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
zify
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(x * y).valuation : ℤ) = HAdd.hAdd (α := ℤ) (↑x.valuation : ℤ) (↑y.valuation : ℤ)

Tactic:
simp [← valuation_coe, Padic.valuation_mul (coe_ne_zero.2 hx) (coe_ne_zero.2 hy)]

Premises used: Iff.mpr, PadicInt.coe_ne_zero, Padic.valuation_mul, PadicInt.valuation_coe
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
zify : (↑(x ^ n).valuation : ℤ) = HMul.hMul (α := ℤ) (↑n : ℤ) (↑x.valuation : ℤ)
⊢ (x ^ n).valuation = n * x.valuation

Tactic:
zify
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ (↑(x ^ n).valuation : ℤ) = HMul.hMul (α := ℤ) (↑n : ℤ) (↑x.valuation : ℤ)

Tactic:
simp [← valuation_coe]

Premises used: PadicInt.valuation_coe
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ‖x‖ = HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑x.valuation : ℤ))

Tactic:
simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx]

Premises used: Iff.mpr, PadicInt.coe_ne_zero, Padic.norm_eq_zpow_neg_valuation, PadicInt.norm_def
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
rw : (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n).valuation + c.valuation = n + c.valuation
rw₁ : n * valuation (p := p) (↑p : ℤ_[p]) + c.valuation = n + c.valuation
rw₂ : n * 1 + c.valuation = n + c.valuation
rw₃ rw₄ : n + c.valuation = n + c.valuation
⊢ (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation = n + c.valuation

Tactic:
rw [valuation_mul (NeZero.ne _) hc, valuation_pow, valuation_p, mul_one]

Premises used: PadicInt.valuation_p, PadicInt.valuation_pow, mul_one, NeZero.ne, PadicInt.valuation_mul
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property) = 1
h' : k = 0
⊢ Eq (α := ℚ_[p]) 0 1

Tactic:
simp [h'] at h
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property) = 1
⊢ k ≠ 0

Tactic:
have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property) = 1
hk : k ≠ 0
⊢ ‖k‖ = 1

Tactic:
rw [norm_eq_padic_norm] at h

Premises used: PadicInt.norm_eq_padic_norm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property) = 1
hk : k ≠ 0
h₁ : ‖k‖ = 1
⊢ k ≠ 0

Tactic:
rw [norm_eq_padic_norm] at h

Premises used: PadicInt.norm_eq_padic_norm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
rw :
  HMul.hMul (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property)
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k⁻¹ ⋯) =
    1
⊢ HMul.hMul (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property)
      (if h : ‖k‖ = 1 then Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k⁻¹ ⋯ else 0) =
    1

Tactic:
rw [dif_pos h]

Premises used: dif_pos
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
apply :
  (↑(HMul.hMul (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property)
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k⁻¹ ⋯)) :
      ℚ_[p]) =
    (↑1 : ℚ_[p])
⊢ HMul.hMul (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property)
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k⁻¹ ⋯) =
    1

Tactic:
apply Subtype.ext_iff.2

Premises used: Iff.mpr, Subtype.ext_iff
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℚ_[p]
property : ‖k‖ ≤ 1
h : ‖k‖ = 1
hk : k ≠ 0
⊢ (↑(HMul.hMul (α := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k property)
          (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) k⁻¹ ⋯)) :
      ℚ_[p]) =
    (↑1 : ℚ_[p])

Tactic:
simp [mul_inv_cancel₀ hk]

Premises used: mul_inv_cancel₀
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
hz : ‖z‖ = 1
rw : z * z.inv = 1
rw₁ rw₂ : Eq (α := ℤ_[p]) 1 1
⊢ z.inv * z = 1

Tactic:
rw [mul_comm, mul_inv hz]

Premises used: PadicInt.mul_inv, mul_comm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
rcases : ∀ (w : ℤ_[p]) (eq : 1 = z * w), ‖z‖ = 1
⊢ ‖z‖ = 1

Tactic:
rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩

Premises used: Iff.mp, isUnit_iff_dvd_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ = 1

Tactic:
le_antisymm (norm_le_one _) ?_

Premises used: le_antisymm, PadicInt.norm_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
refine : 1 ≤ ‖z‖
⊢ ‖z‖ = 1

Tactic:
refine le_antisymm (norm_le_one _) ?_

Premises used: le_antisymm, PadicInt.norm_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
⊢ ‖z‖ * ‖w‖ ≤ ‖z‖ * 1

Tactic:
have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z)
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖ * 1
rwa : ∀ (this : ‖z‖ * ‖w‖ ≤ ‖z‖), 1 ≤ ‖z‖
rwa₁ : ∀ (this : ‖z * w‖ ≤ ‖z‖), 1 ≤ ‖z‖
rwa₂ : ∀ (this : norm (E := ℤ_[p]) 1 ≤ ‖z‖), 1 ≤ ‖z‖
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : 1 ≤ ‖z‖), 1 ≤ ‖z‖
⊢ 1 ≤ ‖z‖

Tactic:
rwa [mul_one, ← norm_mul, ← eq, norm_one] at this

Premises used: NormOneClass.norm_one, norm_mul, mul_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
hz1 : ‖z1‖ < 1
hz2 : ‖z2‖ < 1
⊢ ‖z1 + z2‖ < 1

Tactic:
lt_of_le_of_lt (nonarchimedean _ _) (max_lt hz1 hz2)

Premises used: lt_of_le_of_lt, PadicInt.nonarchimedean, max_lt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
hz2 : ‖z2‖ < 1
⊢ ‖z1 * z2‖ = ‖z1‖ * ‖z2‖

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) z ↔ ‖z‖ < 1

Tactic:
simp [norm_le_one z, nonunits, isUnit_iff]

Premises used: nonunits, PadicInt.isUnit_iff, PadicInt.norm_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ¬IsUnit z ↔ ‖z‖ < 1

Tactic:
simpa using mem_nonunits

Premises used: PadicInt.mem_nonunits
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℚ_[p]
h : ‖u‖ = 1
⊢ (↑(mkUnits h) : ℤ_[p]) = Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) u ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℚ_[p]
h : ‖u‖ = 1
⊢ (↑(↑(mkUnits h) : ℤ_[p]) : ℚ_[p]) = u

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℤ_[p]ˣ
⊢ IsUnit (↑u : ℤ_[p])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x_1 y x : ℤ_[p]
hx : x ≠ 0
u : ℚ_[p] := (↑x : ℚ_[p]) * HPow.hPow (α := ℚ_[p]) (β := ℤ) (↑p : ℚ_[p]) (-(↑x.valuation : ℤ))
⊢ ‖u‖ = 1

Tactic:
simp [u, hx, pow_ne_zero _ (NeZero.ne _), norm_eq_zpow_neg_valuation]

Premises used: PadicInt.norm_eq_zpow_neg_valuation, pow_ne_zero, NeZero.ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (↑(↑(unitCoeff hx) : ℤ_[p]) : ℚ_[p]) =
    (↑x : ℚ_[p]) * HPow.hPow (α := ℚ_[p]) (β := ℤ) (↑p : ℚ_[p]) (-(↑x.valuation : ℤ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
a :
  Eq (α := ℚ_[p]) ((fun (a : { x : ℚ_[p] // ‖x‖ ≤ 1 }) ↦ (↑a : ℚ_[p])) x)
    ((fun (a : { x : ℚ_[p] // ‖x‖ ≤ 1 }) ↦ (↑a : ℚ_[p]))
      ((↑(unitCoeff hx) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) x.valuation))
⊢ x = (↑(unitCoeff hx) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) x.valuation

Tactic:
apply Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
a :
  (↑x : ℚ_[p]) =
    (↑x : ℚ_[p]) * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) (HAdd.hAdd (α := ℤ) (-(↑x.valuation : ℤ)) (↑x.valuation : ℤ))
a₁ : Ne (α := ℚ_[p]) (↑p : ℚ_[p]) 0
⊢ (↑x : ℚ_[p]) = (↑(↑(unitCoeff hx) : ℤ_[p]) : ℚ_[p]) * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) x.valuation

Tactic:
rw [unitCoeff_coe, mul_assoc, ← zpow_natCast, ← zpow_add₀]

Premises used: zpow_natCast, mul_assoc, zpow_add₀, PadicInt.unitCoeff_coe
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (↑x : ℚ_[p]) =
    (↑x : ℚ_[p]) * HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) (HAdd.hAdd (α := ℤ) (-(↑x.valuation : ℤ)) (↑x.valuation : ℤ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ Ne (α := ℚ_[p]) (↑p : ℚ_[p]) 0

Tactic:
NeZero.ne _

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ Ne (α := ℚ_[p]) (↑p : ℚ_[p]) 0

Tactic:
exact NeZero.ne _

Premises used: NeZero.ne