awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n
⊢ (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum
have h₁ : n = n - k + k
Tactic: convert! @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ ‹_›
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
have rw : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a.natAbs
Tactic: rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff_of_ne_one hp, ← Int.natCast_dvd,
    Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
a : ℤ
rw : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a.natAbs
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
have rw₁ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a.natAbs = 0 ∨ n ≤ padicValNat p a.natAbs
Tactic: rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff_of_ne_one hp, ← Int.natCast_dvd,
    Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
have rw₂ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ p ^ n ∣ a.natAbs
Tactic: rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff_of_ne_one hp, ← Int.natCast_dvd,
    Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
have rw₃ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ (↑(p ^ n) : ℤ) ∣ a
Tactic: rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff_of_ne_one hp, ← Int.natCast_dvd,
    Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a
have rw₄ : HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ a
Tactic: rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff_of_ne_one hp, ← Int.natCast_dvd,
    Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
a : ℤ
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
have pos : ∀ (hp : p = 1), HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
Tactic: by_cases hp : p = 1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
a : ℤ
pos : ∀ (hp : p = 1), HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
have neg : ∀ (hp : ¬p = 1), HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
Tactic: by_cases hp : p = 1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
a : ℤ
hp : p = 1
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
have pos : 1 ∣ a
Tactic: rw [hp, Nat.cast_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (padicValInt p a) ∣ a
have neg : a = 0 ∨ padicValInt p a ≤ padicValInt p a
Tactic: rw [padicValInt_dvd_iff_of_ne_one hp]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs
have a₁ : a.natAbs ≠ 0
Tactic: rw [Int.natAbs_mul, padicValNat.mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
a₁ : a.natAbs ≠ 0
⊢ padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs
have a₂ : b.natAbs ≠ 0
Tactic: rw [Int.natAbs_mul, padicValNat.mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p (a * (↑p : ℤ)) = padicValInt p a + 1
have rw : padicValInt p a + padicValInt p (↑p : ℤ) = padicValInt p a + 1
Tactic: rw [padicValInt.mul ha (Int.natCast_ne_zero.mpr hp.out.ne_zero)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ (↑(padicValNat p n) : ℕ∞) = emultiplicity p n
have rw : padicValNat p n ≤ padicValNat p n ∧ ¬padicValNat p n + 1 ≤ padicValNat p n
Tactic: rw [eq_comm, emultiplicity_eq_coe, pow_dvd_iff_le_padicValNat hp hn,
    pow_dvd_iff_le_padicValNat hp hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
⊢ (emultiplicity p n).toNat = padicValNat p n
have inl : (emultiplicity 1 n).toNat = padicValNat 1 n
Tactic: rcases eq_or_ne p 1 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
inl : (emultiplicity 1 n).toNat = padicValNat 1 n
⊢ (emultiplicity p n).toNat = padicValNat p n
have inr : ∀ (hp : p ≠ 1), (emultiplicity p n).toNat = padicValNat p n
Tactic: rcases eq_or_ne p 1 with rfl | hp
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
hp : p ≠ 1
⊢ (emultiplicity p n).toNat = padicValNat p n
have inr : (emultiplicity p 0).toNat = padicValNat p 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
hp : p ≠ 1
inr : (emultiplicity p 0).toNat = padicValNat p 0
⊢ (emultiplicity p n).toNat = padicValNat p n
have inr₁ : ∀ (hn : n ≠ 0), (emultiplicity p n).toNat = padicValNat p n
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
have inl : padicValNat p 0 = 0 ↔ p = 1 ∨ Eq (α := ℕ) 0 0 ∨ ¬p ∣ 0
Tactic: rcases eq_or_ne n 0 with rfl | hn₀
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
inl : padicValNat p 0 = 0 ↔ p = 1 ∨ Eq (α := ℕ) 0 0 ∨ ¬p ∣ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
have inr : ∀ (hn₀ : n ≠ 0), padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Tactic: rcases eq_or_ne n 0 with rfl | hn₀
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
have inr : padicValNat 1 n = 0 ↔ Eq (α := ℕ) 1 1 ∨ n = 0 ∨ ¬1 ∣ n
Tactic: rcases eq_or_ne p 1 with rfl | hp₁
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
p n : ℕ
hn₀ : n ≠ 0
inr : padicValNat 1 n = 0 ↔ Eq (α := ℕ) 1 1 ∨ n = 0 ∨ ¬1 ∣ n
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
have inr₁ : ∀ (hp₁ : p ≠ 1), padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Tactic: rcases eq_or_ne p 1 with rfl | hp₁
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList
have rw : n ≤ padicValNat a b ↔ (↑n : ℕ∞) ≤ emultiplicity a b
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
Goal:
a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
rw : n ≤ padicValNat a b ↔ (↑n : ℕ∞) ≤ emultiplicity a b
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList
have rw₁ : n ≤ padicValNat a b ↔ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
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) : ℕ∞)
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList
have rw₂ : n ≤ padicValNat a b ↔ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(padicValNat a b) : ℕ∞)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Defs (goal)
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) : ℕ∞)
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList
have rw₃ : n ≤ padicValNat a b ↔ n ≤ padicValNat a b
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ TotallyBounded (α := ℤ_[p]) Set.univ
have refine : ∀ (ε : ℝ) (hε : ε > 0), ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)
Tactic: refine Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
⊢ ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)
have obtain : ∀ (k : ℕ) (hk : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑k : ℤ)) < ε),
  ∃ (t : Set ℤ_[p]), t.Finite ∧ Subset (α := Set ℤ_[p]) Set.univ (⋃ y ∈ t, ball y ε)
Tactic: obtain ⟨k, hk⟩ := exists_pow_neg_lt p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.ProperSpace (goal)
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 ε)
have 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
Tactic: refine ⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩