awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
rw :
  (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
      padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]

Premises used: Nat.mul_sub_left_distrib, Nat.factorial_mul_factorial_dvd_factorial, Nat.factorial_ne_zero, padicValNat.div_of_dvd, padicValNat.mul, Nat.mul_add
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
simp :
  n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
⊢ (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
simp only [sub_one_mul_padicValNat_factorial]

Premises used: sub_one_mul_padicValNat_factorial
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
rw :
  n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₁ :
  n + k - (p.digits (n + k)).sum - (k + (n - (p.digits n).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₂ :
  n + k - (p.digits (n + k)).sum - (k + n - (p.digits n).sum - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₃ :
  n + k - (p.digits (n + k)).sum - (k + n - ((p.digits n).sum + (p.digits k).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₄ :
  n + k - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (n + k)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₅ :
  n + k - (k + n - ((p.digits n).sum + (p.digits k).sum) + (p.digits (n + k)).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₆ :
  n + k - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (n + k)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
rw₇ :
  k + n - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
rw₈ :
  k + n - (k + n) + ((p.digits n).sum + (p.digits k).sum) - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
rw₉ :
  0 + ((p.digits n).sum + (p.digits k).sum) - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
rw₁₀ :
  (p.digits n).sum + (p.digits k).sum - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
rw₁₁ rw₁₂ :
  (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]

Premises used: Nat.le_refl, Nat.sub_add_eq, Nat.add_sub_assoc, Nat.sub_add_comm, Nat.sub_sub, zero_add, add_comm, Nat.sub_self, HAdd.hAdd, tsub_tsub_assoc, Nat.sub_right_comm, Nat.digit_sum_le, Nat.add_sub_cancel
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ (p - 1) * padicValNat p ((n - k + k).choose k) =
    (p.digits k).sum + (p.digits (n - k)).sum - (p.digits (n - k + k)).sum

Tactic:
@sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ ‹_›

Premises used: sub_one_mul_padicValNat_choose_eq_sub_sum_digits'
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
h₁ h₂ : n = n - k + k
⊢ (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

Tactic:
convert! @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ ‹_›

Premises used: sub_one_mul_padicValNat_choose_eq_sub_sum_digits'
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ n = n - k + k

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
rw : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a.natAbs
rw₁ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a.natAbs = 0 ∨ n ≤ padicValNat p a.natAbs
rw₂ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ p ^ n ∣ a.natAbs
rw₃ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ (↑(p ^ n) : ℤ) ∣ a
rw₄ rw₅ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

Tactic:
rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff_of_ne_one hp, ← Int.natCast_dvd,
    Int.natCast_pow]

Premises used: padicValNat_dvd_iff_of_ne_one, padicValInt, Int.natCast_pow, Int.natAbs_eq_zero, Int.natCast_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

Tactic:
padicValInt_dvd_iff_of_ne_one hp.out.ne_one n a

Premises used: padicValInt_dvd_iff_of_ne_one, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
pos : ∀ (hp : p = 1), HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
neg : ∀ (hp : ¬p = 1), HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a

Tactic:
by_cases hp : p = 1
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
hp : p = 1
pos : 1 ∣ a
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a

Tactic:
rw [hp, Nat.cast_one, one_pow]

Premises used: one_pow, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ∣ a

Tactic:
one_dvd _

Premises used: one_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ∣ a

Tactic:
exact one_dvd _

Premises used: one_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
hp : ¬p = 1
neg : a = 0 ∨ padicValInt p a ≤ padicValInt p a
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a

Tactic:
rw [padicValInt_dvd_iff_of_ne_one hp]

Premises used: padicValInt_dvd_iff_of_ne_one
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a

Tactic:
Or.inr le_rfl

Premises used: le_rfl, Or.inr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a

Tactic:
exact Or.inr le_rfl

Premises used: le_rfl, Or.inr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicValInt p (↑p : ℤ) = 1

Tactic:
padicValInt.self hp.out.one_lt

Premises used: Nat.Prime.one_lt, padicValInt.self, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
a₁ : a.natAbs ≠ 0
a₂ : b.natAbs ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs

Tactic:
rw [Int.natAbs_mul, padicValNat.mul]

Premises used: Int.natAbs_mul, padicValNat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
a₁ a₂ a₃ a₄ : a ≠ 0
⊢ a.natAbs ≠ 0

Tactic:
rwa [Int.natAbs_ne_zero]

Premises used: Int.natAbs_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb a₁ a₂ a₃ a₄ : b ≠ 0
⊢ b.natAbs ≠ 0

Tactic:
rwa [Int.natAbs_ne_zero]

Premises used: Int.natAbs_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
rw : padicValInt p a + padicValInt p (↑p : ℤ) = padicValInt p a + 1
⊢ padicValInt p (a * (↑p : ℤ)) = padicValInt p a + 1

Tactic:
rw [padicValInt.mul ha (Int.natCast_ne_zero.mpr hp.out.ne_zero)]

Premises used: Iff.mpr, Int.natCast_ne_zero, Nat.Prime.ne_zero, padicValInt.mul, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p a + padicValInt p (↑p : ℤ) = padicValInt p a + 1

Tactic:
simp only [padicValInt.of_nat, padicValNat_self]

Premises used: padicValNat_self, padicValInt.of_nat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
rw : padicValNat p n ≤ padicValNat p n ∧ ¬padicValNat p n + 1 ≤ padicValNat p n
⊢ (↑(padicValNat p n) : ℕ∞) = emultiplicity p n

Tactic:
rw [eq_comm, emultiplicity_eq_coe, pow_dvd_iff_le_padicValNat hp hn,
    pow_dvd_iff_le_padicValNat hp hn]

Premises used: Nat.pow_dvd_iff_le_padicValNat, eq_comm, emultiplicity_eq_coe
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ padicValNat p n ∧ ¬padicValNat p n + 1 ≤ padicValNat p n

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
inl : (emultiplicity 1 n).toNat = padicValNat 1 n
inr : ∀ (hp : p ≠ 1), (emultiplicity p n).toNat = padicValNat p n
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
rcases eq_or_ne p 1 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
n : ℕ
⊢ (emultiplicity 1 n).toNat = padicValNat 1 n

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
hp : p ≠ 1
inr : (emultiplicity p 0).toNat = padicValNat p 0
inr₁ : ∀ (hn : n ≠ 0), (emultiplicity p n).toNat = padicValNat p n
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
hp : p ≠ 1
⊢ (emultiplicity p 0).toNat = padicValNat p 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
simp [← padicValNat_eq_emultiplicity_of_ne_one, *]

Premises used: padicValNat_eq_emultiplicity_of_ne_one
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ padicValNat p n = multiplicity p n

Tactic:
.symm <| multiplicity_eq_of_emultiplicity_eq_some <| .symm <|
    padicValNat_eq_emultiplicity_of_ne_one hp hn

Premises used: padicValNat_eq_emultiplicity_of_ne_one, Eq.symm, multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n = multiplicity p n

Tactic:
padicValNat_def' hp.out.ne_one hn

Premises used: Nat.Prime.ne_one, padicValNat_def', Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
⊢ (↑(padicValNat p n) : ℕ∞) = emultiplicity p n

Tactic:
padicValNat_eq_emultiplicity_of_ne_one hp.out.ne_one hn

Premises used: Nat.Prime.ne_one, padicValNat_eq_emultiplicity_of_ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
⊢ padicValNat p 0 = 0

Tactic:
padicValNat_zero_right p

Premises used: padicValNat_zero_right
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
⊢ padicValNat p 1 = 0

Tactic:
padicValNat_one_right p

Premises used: padicValNat_one_right
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
inl : padicValNat p 0 = 0 ↔ p = 1 ∨ Eq (α := ℕ) 0 0 ∨ ¬p ∣ 0
inr : ∀ (hn₀ : n ≠ 0), padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p : ℕ
⊢ padicValNat p 0 = 0 ↔ p = 1 ∨ Eq (α := ℕ) 0 0 ∨ ¬p ∣ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
hn₀ : n ≠ 0
inr : padicValNat 1 n = 0 ↔ Eq (α := ℕ) 1 1 ∨ n = 0 ∨ ¬1 ∣ n
inr₁ : ∀ (hp₁ : p ≠ 1), padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
rcases eq_or_ne p 1 with rfl | hp₁

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat 1 n = 0 ↔ Eq (α := ℕ) 1 1 ∨ n = 0 ∨ ¬1 ∣ n

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
simpa [*] using pow_dvd_iff_le_padicValNat (k := 1) hp₁ hn₀ |>.symm |>.not

Premises used: Iff.not, Nat.pow_dvd_iff_le_padicValNat, Iff.symm
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ (↑n : ℕ∞) ≤ emultiplicity a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
(replicate_subperm_primeFactorsList_iff ha hb).trans
    pow_dvd_iff_le_emultiplicity |>.symm

Premises used: pow_dvd_iff_le_emultiplicity, Iff.trans, Nat.replicate_subperm_primeFactorsList_iff, Iff.symm
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Defs
Goal:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
rw : n ≤ padicValNat a b ↔ (↑n : ℕ∞) ≤ emultiplicity a b
rw₁ : n ≤ padicValNat a b ↔ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
rw₂ : n ≤ padicValNat a b ↔ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(padicValNat a b) : ℕ∞)
rw₃ rw₄ : n ≤ padicValNat a b ↔ n ≤ padicValNat a b
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
rw [← le_emultiplicity_iff_replicate_subperm_primeFactorsList ha hb,
    Nat.finiteMultiplicity_iff.2 ⟨ha.ne_one, Nat.pos_of_ne_zero hb⟩
      |>.emultiplicity_eq_multiplicity, ← padicValNat_def' ha.ne_one hb,
    Nat.cast_le]

Premises used: Iff.mpr, FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.pos_of_ne_zero, Nat.Prime.ne_one, padicValNat_def', And.intro, Nat.cast_le, le_emultiplicity_iff_replicate_subperm_primeFactorsList, Nat.finiteMultiplicity_iff
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ TotallyBounded (α := ℤ_[p]) Set.univ

Tactic:
Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)

Premises used: Iff.mpr, Metric.totallyBounded_iff
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
refine : ∀ (ε : ℝ) (hε : ε > 0), ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)
⊢ TotallyBounded (α := ℤ_[p]) Set.univ

Tactic:
refine Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)

Premises used: Iff.mpr, Metric.totallyBounded_iff
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
obtain :
  ∀ (k : ℕ) (hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε),
    ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)
⊢ ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)

Tactic:
obtain ⟨k, hk⟩ := exists_pow_neg_lt p hε

Premises used: PadicInt.exists_pow_neg_lt
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
⊢ ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)

Tactic:
⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩

Premises used: Nat.cast, Finset.range, Set.toFinite, SetLike.coe, HPow.hPow, And.intro, Exists.intro, Set.image
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
refine :
  ∀ (z : ℤ_[p]),
    Membership.mem (γ := Set ℤ_[p]) Set.univ z →
      Membership.mem (γ := Set ℤ_[p])
        (⋃ (y : ℤ_[p]),
          ⋃ (_ : Membership.mem (γ := Set ℤ_[p]) (Nat.cast '' (↑(Finset.range (p ^ k)) : Set ℕ)) y), ball y ε)
        z
⊢ ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)

Tactic:
refine ⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
simp : ∃ x ∈ (↑(Finset.range (p ^ k)) : Set ℕ), dist z (↑x : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε
⊢ Membership.mem (γ := Set ℤ_[p])
    (⋃ (y : ℤ_[p]), ⋃ (_ : Membership.mem (γ := Set ℤ_[p]) (Nat.cast '' (↑(Finset.range (p ^ k)) : Set ℕ)) y), ball y ε)
    z

Tactic:
simp only [PadicInt, Set.mem_iUnion, Metric.mem_ball, exists_prop, Set.exists_mem_image]

Premises used: PadicInt, Set.mem_iUnion, exists_prop, Metric.mem_ball, Set.exists_mem_image
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
⊢ ∃ x ∈ (↑(Finset.range (p ^ k)) : Set ℕ), dist z (↑x : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε

Tactic:
⟨z.appr k, ?_, ?_⟩

Premises used: And.intro, Exists.intro, PadicInt.appr
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
refine_1 : z.appr k ∈ (↑(Finset.range (p ^ k)) : Set ℕ)
refine_2 : dist z (↑(z.appr k) : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε
⊢ ∃ x ∈ (↑(Finset.range (p ^ k)) : Set ℕ), dist z (↑x : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε

Tactic:
refine ⟨z.appr k, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
⊢ z.appr k ∈ (↑(Finset.range (p ^ k)) : Set ℕ)

Tactic:
simpa only [Finset.mem_coe, Finset.mem_range] using z.appr_lt k

Premises used: Finset.mem_range, PadicInt.appr_lt, Finset.mem_coe
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
⊢ dist z (↑(z.appr k) : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε

Tactic:
(((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk

Premises used: Iff.mpr, PadicInt.appr_spec, PadicInt, HSub.hSub, Nat.cast, PadicInt.norm_le_pow_iff_mem_span_pow, PadicInt.appr, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε
z : ℤ_[p]
h : Membership.mem (γ := Set ℤ_[p]) Set.univ z
⊢ dist z (↑(z.appr k) : { x : ℚ_[p] // ‖x‖ ≤ 1 }) < ε

Tactic:
exact (((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk

Premises used: Iff.mpr, PadicInt.appr_spec, HSub.hSub, Nat.cast, PadicInt.norm_le_pow_iff_mem_span_pow, PadicInt.appr, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : TotallyBounded (α := ℤ_[p]) Set.univ ∧ IsComplete (α := ℤ_[p]) Set.univ
⊢ CompactSpace ℤ_[p]

Tactic:
rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete]

Premises used: isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ TotallyBounded (α := ℤ_[p]) Set.univ ∧ IsComplete (α := ℤ_[p]) Set.univ

Tactic:
⟨totallyBounded_univ p, complete_univ⟩

Premises used: complete_univ, And.intro, PadicInt.totallyBounded_univ
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ TotallyBounded (α := ℤ_[p]) Set.univ ∧ IsComplete (α := ℤ_[p]) Set.univ

Tactic:
exact ⟨totallyBounded_univ p, complete_univ⟩
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
suffices : LocallyCompactSpace ℚ_[p]
⊢ ProperSpace ℚ_[p]

Tactic:
suffices LocallyCompactSpace ℚ_[p] from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace _
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) (closedBall 0 1)

Tactic:
have : closedBall 0 1 ∈ 𝓝 (0 : ℚ_[p]) := closedBall_mem_nhds _ zero_lt_one
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) (closedBall 0 1)
⊢ Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) {y : ℚ_[p] | ‖y‖ ≤ 1}

Tactic:
simp only [closedBall, dist_eq_norm_sub, sub_zero] at this

Premises used: dist_eq_norm_sub, sub_zero, Metric.closedBall
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) {y : ℚ_[p] | ‖y‖ ≤ 1}
⊢ LocallyCompactSpace ℚ_[p]

Tactic:
IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup ?_ this

Premises used: IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) {y : ℚ_[p] | ‖y‖ ≤ 1}
refine : IsCompact (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}
⊢ LocallyCompactSpace ℚ_[p]

Tactic:
refine IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup ?_ this

Premises used: IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup
-- Module: Mathlib.NumberTheory.Padics.ProperSpace
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
this : Membership.mem (γ := Filter ℚ_[p]) (𝓝 0) {y : ℚ_[p] | ‖y‖ ≤ 1}
⊢ IsCompact (X := ℚ_[p]) {y : ℚ_[p] | ‖y‖ ≤ 1}

Tactic:
simpa only [isCompact_iff_compactSpace] using PadicInt.compactSpace p

Premises used: isCompact_iff_compactSpace, PadicInt.compactSpace
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ r.num * r.den.gcdA p % (↑p : ℤ) < |(↑p : ℤ)|

Tactic:
Int.emod_lt_abs _ _

Premises used: Int.emod_lt_abs
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : Eq (α := ℤ) (↑p : ℤ) |(↑p : ℤ)|
convert_3 : Ne (α := ℤ) (↑p : ℤ) 0
⊢ modPart p r < (↑p : ℤ)

Tactic:
convert! Int.emod_lt_abs _ _

Premises used: Int.emod_lt_abs
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ Eq (α := ℤ) (↑p : ℤ) |(↑p : ℤ)|

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ Ne (α := ℤ) (↑p : ℤ) 0

Tactic:
mod_cast hp_prime.1.ne_zero

Premises used: congrArg, cast, Ne, Nat.cast, Nat.Prime.ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ Ne (α := ℤ) (↑p : ℤ) 0

Tactic:
exact mod_cast hp_prime.1.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ 0 ≤ modPart p r

Tactic:
Int.emod_nonneg _ <| mod_cast hp_prime.1.ne_zero

Premises used: congrArg, cast, PadicInt.modPart, Ne, Nat.cast, Nat.Prime.ne_zero, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Not, Int.emod_nonneg, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : norm (E := ℚ_[p]) (↑r : ℚ_[p]) ≤ 1
rw : Eq (α := ZMod p) (↑(r.num - r.num * r.den.gcdA p % (↑p : ℤ) * (↑r.den : ℤ)) : ZMod p) 0
⊢ (↑p : ℤ) ∣ r.num - r.num * r.den.gcdA p % (↑p : ℤ) * (↑r.den : ℤ)

Tactic:
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd