awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
rw : norm (E := ℤ_[p]) (↑r.den : ℤ_[p]) = 1
⊢ IsUnit (M := ℤ_[p]) (↑r.den : ℤ_[p])

Tactic:
rw [isUnit_iff]

Premises used: PadicInt.isUnit_iff
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
apply : 1 ≤ norm (E := ℚ_[p]) (↑(↑r.den : ℤ_[p]) : ℚ_[p])
⊢ norm (E := ℤ_[p]) (↑r.den : ℤ_[p]) = 1

Tactic:
apply le_antisymm (r.den : ℤ_[p]).2

Premises used: Rat.den, Nat.cast, le_antisymm, Subtype.property
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
rw : ¬norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
⊢ 1 ≤ norm (E := ℚ_[p]) (↑(↑r.den : ℤ_[p]) : ℚ_[p])

Tactic:
rw [← not_lt, coe_natCast]

Premises used: PadicInt.coe_natCast, not_lt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
e_a : HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p]) = (↑r.num : ℚ_[p])
⊢ ‖HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p])‖ = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])

Tactic:
congr
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
e_a e_a₁ e_a₂ e_a₃ e_a₄ e_a₅ :
  ∀ (h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1) (norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1),
    r * (↑r.den : ℚ) = (↑r.num : ℚ)
⊢ HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p]) = (↑r.num : ℚ_[p])

Tactic:
rw_mod_cast [@Rat.mul_den_eq_num r]

Premises used: Rat.mul_den_eq_num
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
⊢ ‖HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p])‖ = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])

Tactic:
have hr : ‖(r * r.den : ℚ_[p])‖ = ‖(r.num : ℚ_[p])‖ := by
    congr
    rw_mod_cast [@Rat.mul_den_eq_num r]
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : ‖HMul.hMul (α := ℚ_[p]) (↑r : ℚ_[p]) (↑r.den : ℚ_[p])‖ = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])

Tactic:
rw [padicNormE.mul] at hr

Premises used: Padic.padicNormE.mul
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) = norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p])

Tactic:
hr.symm

Premises used: Eq.symm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < HMul.hMul (α := ℝ) 1 1

Tactic:
mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one

Premises used: zero_lt_one, mul_lt_mul', norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
⊢ HMul.hMul (α := ℝ) 1 1 = 1

Tactic:
mul_one 1

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1

Tactic:
calc
      _ = _ := hr.symm
      _ < 1 * 1 := mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one
      _ = 1 := mul_one 1

Premises used: zero_lt_one, mul_lt_mul', mul_one, OfNat.ofNat, Eq.symm, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1

Tactic:
have key : ‖(r.num : ℚ_[p])‖ < 1 := by
    calc
      _ = _ := hr.symm
      _ < 1 * 1 := mul_lt_mul' h norm_denom_lt (norm_nonneg _) zero_lt_one
      _ = 1 := mul_one 1
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
key : norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1
simp : norm (E := ℚ_[p]) (↑(↑r.num : ℤ_[p]) : ℚ_[p]) < 1 ∧ norm (E := ℚ_[p]) (↑(↑(↑r.den : ℤ) : ℤ_[p]) : ℚ_[p]) < 1
⊢ (↑p : ℤ) ∣ r.num ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)

Tactic:
simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]

Premises used: PadicInt.norm_int_lt_one_iff_dvd, PadicInt.padic_norm_e_of_padicInt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
key : norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1
⊢ norm (E := ℚ_[p]) (↑(↑r.num : ℤ_[p]) : ℚ_[p]) < 1 ∧ norm (E := ℚ_[p]) (↑(↑(↑r.den : ℤ) : ℤ_[p]) : ℚ_[p]) < 1

Tactic:
⟨key, norm_denom_lt⟩

Premises used: And.intro
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
key : norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1
⊢ norm (E := ℚ_[p]) (↑(↑r.num : ℤ_[p]) : ℚ_[p]) < 1 ∧ norm (E := ℚ_[p]) (↑(↑(↑r.den : ℤ) : ℤ_[p]) : ℚ_[p]) < 1

Tactic:
exact ⟨key, norm_denom_lt⟩
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
key : norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1
⊢ (↑p : ℤ) ∣ r.num ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)

Tactic:
have : ↑p ∣ r.num ∧ (p : ℤ) ∣ r.den := by
    simp only [← norm_int_lt_one_iff_dvd, ← padic_norm_e_of_padicInt]
    exact ⟨key, norm_denom_lt⟩
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
key : norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1
this : (↑p : ℤ) ∣ r.num ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)
apply : p ∣ 1
⊢ False

Tactic:
apply hp_prime.1.not_dvd_one

Premises used: Nat.Prime.not_dvd_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
norm_denom_lt : norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) < 1
hr : norm (E := ℚ_[p]) (↑r : ℚ_[p]) * norm (E := ℚ_[p]) (↑r.den : ℚ_[p]) = norm (E := ℚ_[p]) (↑r.num : ℚ_[p])
key : norm (E := ℚ_[p]) (↑r.num : ℚ_[p]) < 1
this : (↑p : ℤ) ∣ r.num ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)
rwa : p ∣ r.num.natAbs.gcd r.den
rwa₁ : p ∣ r.num.natAbs ∧ p ∣ r.den
rwa₂ : (↑p : ℤ) ∣ r.num ∧ p ∣ r.den
rwa₃ rwa₄ rwa₅ rwa₆ : (↑p : ℤ) ∣ r.num ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)
⊢ p ∣ 1

Tactic:
rwa [← r.reduced.gcd_eq_one, Nat.dvd_gcd_iff, ← Int.natCast_dvd, ← Int.natCast_dvd_natCast]

Premises used: Nat.dvd_gcd_iff, Rat.reduced, Nat.Coprime.gcd_eq_one, Int.natCast_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
rw : LT.lt (α := ℝ) 1 (↑p : ℝ)
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔ n ≤ x.valuation

Tactic:
rw [norm_eq_zpow_neg_valuation hx, zpow_le_zpow_iff_right₀, neg_le_neg_iff, Nat.cast_le]

Premises used: PadicInt.norm_eq_zpow_neg_valuation, zpow_le_zpow_iff_right₀, Nat.cast_le, neg_le_neg_iff
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ 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
n : ℕ
⊢ 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]
hx : x ≠ 0
n : ℕ
rw : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x ↔ n ≤ x.valuation
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x ↔ n ≤ x.valuation

Tactic:
rw [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
mp : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x → n ≤ x.valuation
mpr : n ≤ x.valuation → HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x ↔ n ≤ x.valuation

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c ≠ 0
this : c ≠ 0
rw : n ≤ n + c.valuation
⊢ n ≤ (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation

Tactic:
rw [valuation_p_pow_mul _ _ this]

Premises used: PadicInt.valuation_p_pow_mul
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c ≠ 0
this : c ≠ 0
⊢ n ≤ n + c.valuation

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c ≠ 0
this : c ≠ 0
⊢ n ≤ n + c.valuation

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c ≠ 0
mp : c ≠ 0
⊢ n ≤ (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation

Tactic:
suffices c ≠ 0 by
      rw [valuation_p_pow_mul _ _ this]
      exact le_self_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c ≠ 0
mp : ∀ (hx : c = 0), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c = 0
⊢ c ≠ 0

Tactic:
contrapose hx
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
mp : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * 0 = 0
mp₁ mp₂ : Eq (α := ℤ_[p]) 0 0
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c = 0

Tactic:
rw [hx, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
mpr :
  n ≤ x.valuation →
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑(unitCoeff hx) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) x.valuation
⊢ n ≤ x.valuation → HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x

Tactic:
nth_rewrite 2 [unitCoeff_spec hx]

Premises used: PadicInt.unitCoeff_spec
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ n ≤ x.valuation →
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑(unitCoeff hx) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) x.valuation

Tactic:
simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _

Premises used: IsUnit.dvd_mul_left, pow_dvd_pow, Units.isUnit
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
pos :
  ∀ (hx : x = 0),
    ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x
neg :
  ∀ (hx : ¬x = 0),
    ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : x = 0
pos :
  norm (E := ℤ_[p]) 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) 0
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x

Tactic:
subst hx
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
pos : 0 ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n
⊢ norm (E := ℤ_[p]) 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) 0

Tactic:
simp only [norm_zero, zpow_neg, zpow_natCast, inv_nonneg, iff_true, Submodule.zero_mem]

Premises used: zpow_natCast, norm_zero, iff_true, inv_nonneg, Submodule.zero_mem, zpow_neg
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n

Tactic:
mod_cast Nat.zero_le _

Premises used: Nat.zero_le, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HPow.hPow, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n

Tactic:
exact mod_cast Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
hx : ¬x = 0
neg : n ≤ x.valuation ↔ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x
neg₁ neg₂ : n ≤ x.valuation ↔ n ≤ x.valuation
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) x

Tactic:
rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]

Premises used: PadicInt.mem_span_pow_iff_le_valuation, PadicInt.norm_le_pow_iff_le_valuation
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖(↑x : ℚ_[p])‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖(↑x : ℚ_[p])‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)

Tactic:
Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _

Premises used: Padic.norm_le_pow_iff_norm_lt_pow_add_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖(↑x : ℚ_[p])‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖(↑x : ℚ_[p])‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)

Tactic:
exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _

Premises used: Padic.norm_le_pow_iff_norm_lt_pow_add_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
rw : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1 + 1)
rw₁ rw₂ : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n
⊢ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1)

Tactic:
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

Premises used: PadicInt.norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1}) x

Tactic:
have := norm_le_pow_iff_mem_span_pow x 1
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this :
  ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1}) x
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔ (↑p : ℤ_[p]) ∣ x

Tactic:
rw [Ideal.mem_span_singleton, pow_one] at this

Premises used: pow_one, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔ (↑p : ℤ_[p]) ∣ x
rw : ‖x‖ < 1 ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)
⊢ ‖x‖ < 1 ↔ (↑p : ℤ_[p]) ∣ x

Tactic:
rw [← this, norm_le_pow_iff_norm_lt_pow_add_one]

Premises used: PadicInt.norm_le_pow_iff_norm_lt_pow_add_one
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔ (↑p : ℤ_[p]) ∣ x
⊢ ‖x‖ < 1 ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)

Tactic:
simp only [zpow_zero, Int.ofNat_zero, Int.natCast_succ, neg_add_cancel, zero_add]

Premises used: zpow_zero, zero_add, Int.ofNat_zero, Int.natCast_succ, neg_add_cancel
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
rw : Dvd.dvd (α := ℤ_[p]) (↑(p ^ n) : ℤ_[p]) (↑a : ℤ_[p]) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a
rw₁ :
  Dvd.dvd (α := ℤ_[p]) (↑(p ^ n) : ℤ_[p]) (↑a : ℤ_[p]) ↔
    norm (E := ℤ_[p]) (↑a : ℤ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
rw₂ :
  Dvd.dvd (α := ℤ_[p]) (↑(p ^ n) : ℤ_[p]) (↑a : ℤ_[p]) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (↑a : ℤ_[p])
rw₃ : Dvd.dvd (α := ℤ_[p]) (↑(p ^ n) : ℤ_[p]) (↑a : ℤ_[p]) ↔ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p])
rw₄ rw₅ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) ↔ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p])
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ (↑a : ℤ_[p]) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a

Tactic:
rw [← Nat.cast_pow, ← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow,
    Ideal.mem_span_singleton, Nat.cast_pow]

Premises used: PadicInt.norm_int_le_pow_iff_dvd, PadicInt.norm_le_pow_iff_mem_span_pow, Nat.cast_pow, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
simp : ∀ (a b : ℤ_[p]), ‖a‖ < 1 → ‖b‖ < 1 → ‖a + b‖ < 1
⊢ ∀ (a b : ℤ_[p]),
    Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) a →
      Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) b → Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) (a + b)

Tactic:
simp only [mem_nonunits]

Premises used: PadicInt.mem_nonunits
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), ‖a‖ < 1 → ‖b‖ < 1 → ‖a + b‖ < 1

Tactic:
fun x y => norm_lt_one_add

Premises used: PadicInt.norm_lt_one_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), ‖a‖ < 1 → ‖b‖ < 1 → ‖a + b‖ < 1

Tactic:
exact fun x y => norm_lt_one_add

Premises used: PadicInt.norm_lt_one_add
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
have : (p : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp.out.one_lt
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
this : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
rwa : ∀ (this : norm (E := ℤ_[p]) (↑p : ℤ_[p]) < 1), Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) (↑p : ℤ_[p])
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) (↑p : ℤ_[p])),
    Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) (↑p : ℤ_[p])
⊢ Membership.mem (γ := Set ℤ_[p]) (nonunits ℤ_[p]) (↑p : ℤ_[p])

Tactic:
rwa [← norm_p, ← mem_nonunits] at this

Premises used: PadicInt.norm_p, PadicInt.mem_nonunits
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : LE.le (α := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
a₁ : LE.le (α := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (maximalIdeal ℤ_[p])
⊢ Eq (α := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : Membership.mem (γ := Submodule ℤ_[p] ℤ_[p]) (maximalIdeal ℤ_[p]) x
⊢ ‖x‖ < 1

Tactic:
simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits] at hx

Premises used: IsLocalRing.mem_maximalIdeal, PadicInt.mem_nonunits
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ‖x‖ < 1
a : (↑p : ℤ_[p]) ∣ x
a₁ a₂ a₃ a₄ : ‖x‖ < 1
⊢ Membership.mem (γ := Submodule ℤ_[p] ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x

Tactic:
rwa [Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]

Premises used: PadicInt.norm_lt_one_iff_dvd, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : (↑p : ℤ_[p]) ∈ (↑(maximalIdeal ℤ_[p]) : Set ℤ_[p])
⊢ LE.le (α := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (maximalIdeal ℤ_[p])

Tactic:
rw [Ideal.span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p : ℤ_[p]) ∈ (↑(maximalIdeal ℤ_[p]) : Set ℤ_[p])

Tactic:
p_nonunit

Premises used: Set.Mem, setOf, nonunits, PadicInt.p_nonunit, Not
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p : ℤ_[p]) ∈ (↑(maximalIdeal ℤ_[p]) : Set ℤ_[p])

Tactic:
exact p_nonunit

Premises used: PadicInt.p_nonunit
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : Ideal.IsPrime (α := ℤ_[p]) (maximalIdeal ℤ_[p])
rw₁ : Ne (α := ℤ_[p]) (↑p : ℤ_[p]) 0
⊢ Prime (M := ℤ_[p]) (↑p : ℤ_[p])

Tactic:
rw [← Ideal.span_singleton_prime, ← maximalIdeal_eq_span_p]

Premises used: PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_prime
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Ideal.IsPrime (α := ℤ_[p]) (maximalIdeal ℤ_[p])

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

Tactic:
NeZero.ne _

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

Tactic:
exact NeZero.ne _

Premises used: NeZero.ne
-- Module: Mathlib.NumberTheory.Padics.PadicIntegers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Irreducible (M := ℤ_[p]) (↑p : ℤ_[p])

Tactic:
Prime.irreducible prime_p

Premises used: Prime.irreducible, PadicInt.prime_p