awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : ∀ (hF : ∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)), padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
i : ℕ
hi : i ∈ S'
⊢ i ∈ Finset.cons s S' Hnot
have rw : i = s ∨ i ∈ S'
Tactic: rw [Finset.cons_eq_insert, Finset.mem_insert]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hS : S.Nonempty
hF : ∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)
hn1 : ∀ (i : ℕ), 0 < F i
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)
have singleton : ∀ (k : ℕ) (hF : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) {k} i → padicValRat p (F j) < padicValRat p (F i)),
  padicValRat p (F j) < padicValRat p (∑ i ∈ {k}, F i)
Tactic: induction hS using Finset.Nonempty.cons_induction with
  | singleton k =>
    rw [Finset.sum_singleton]
    exact hF k (by simp)
  | cons s S' Hnot Hne Hind =>
    rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]
    exact padicValRat.lt_add_of_lt
      (ne_of_gt (add_pos (hn1 s) (Finset.sum_pos (fun i _ => hn1 i) Hne)))
      (hF _ (by simp [Finset.mem_insert, true_or]))
      (Hind (fun i hi => hF _ (by rw [Finset.cons_eq_insert, Finset.mem_insert]; exact Or.inr hi)))
Cleared hypotheses: hS, hF
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hS : S.Nonempty
hF : ∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)
hn1 : ∀ (i : ℕ), 0 < F i
singleton :
  ∀ (k : ℕ) (hF : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) {k} i → padicValRat p (F j) < padicValRat p (F i)),
    padicValRat p (F j) < padicValRat p (∑ i ∈ {k}, F i)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)
have cons : ∀ (s : ℕ) (S' : Finset ℕ) (Hnot : s ∉ S') (Hne : S'.Nonempty)
  (Hind :
    ∀ (hF : ∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)), padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i))
  (hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)),
  padicValRat p (F j) < padicValRat p (∑ i ∈ Finset.cons s S' Hnot, F i)
Tactic: induction hS using Finset.Nonempty.cons_induction with
  | singleton k =>
    rw [Finset.sum_singleton]
    exact hF k (by simp)
  | cons s S' Hnot Hne Hind =>
    rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]
    exact padicValRat.lt_add_of_lt
      (ne_of_gt (add_pos (hn1 s) (Finset.sum_pos (fun i _ => hn1 i) Hne)))
      (hF _ (by simp [Finset.mem_insert, true_or]))
      (Hind (fun i hi => hF _ (by rw [Finset.cons_eq_insert, Finset.mem_insert]; exact Or.inr hi)))
Cleared hypotheses: hS, hF
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
have inl : ∀ (h : b ∣ 0), padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
inl : ∀ (h : b ∣ 0), padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
have inr : ∀ (ha : a ≠ 0), padicValNat p (a / b) = padicValNat p a - padicValNat p b
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
have inr : ∀ (k : ℕ) (ha : b * k ≠ 0), padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
Tactic: obtain ⟨k, rfl⟩ := h
Cleared hypotheses: a, h, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
have hb : b ≠ 0
Tactic: obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
have hk : k ≠ 0
Tactic: obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
have inr : padicValNat p (k * b / b) = padicValNat p (k * b) - padicValNat p b
Tactic: rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
inr : padicValNat p (k * b / b) = padicValNat p (k * b) - padicValNat p b
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
have inr₁ : padicValNat p k = padicValNat p (k * b) - padicValNat p b
Tactic: rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
inr : padicValNat p (k * b / b) = padicValNat p (k * b) - padicValNat p b
inr₁ : padicValNat p k = padicValNat p (k * b) - padicValNat p b
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
have inr₂ : padicValNat p k = padicValNat p k + padicValNat p b - padicValNat p b
Tactic: rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
inr : padicValNat p (k * b / b) = padicValNat p (k * b) - padicValNat p b
inr₁ : padicValNat p k = padicValNat p (k * b) - padicValNat p b
inr₂ : padicValNat p k = padicValNat p k + padicValNat p b - padicValNat p b
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
have inr₃ : padicValNat p k = padicValNat p k
Tactic: rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p (b / p) = padicValNat p b - 1
have rw : padicValNat p b - padicValNat p p = padicValNat p b - 1
Tactic: rw [padicValNat.div_of_dvd dvd, padicValNat_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
rw : padicValNat p b - padicValNat p p = padicValNat p b - 1
⊢ padicValNat p (b / p) = padicValNat p b - 1
have rw₁ : padicValNat p b - 1 = padicValNat p b - 1
Tactic: rw [padicValNat.div_of_dvd dvd, padicValNat_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p (p ^ n) = n
have rw : n * padicValNat p p = n
Tactic: rw [padicValNat.pow _ (@Fact.out p.Prime).ne_zero, padicValNat_self, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : n * padicValNat p p = n
⊢ padicValNat p (p ^ n) = n
have rw₁ : n * 1 = n
Tactic: rw [padicValNat.pow _ (@Fact.out p.Prime).ne_zero, padicValNat_self, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : n * padicValNat p p = n
rw₁ : n * 1 = n
⊢ padicValNat p (p ^ n) = n
have rw₂ : n = n
Tactic: rw [padicValNat.pow _ (@Fact.out p.Prime).ne_zero, padicValNat_self, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a
have rw : padicValNat p b - padicValNat p (p ^ a) = padicValNat p b - a
Tactic: rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ^ a ∣ b
rw : padicValNat p b - padicValNat p (p ^ a) = padicValNat p b - a
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a
have rw₁ : padicValNat p b - a = padicValNat p b - a
Tactic: rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p (b / m) = padicValNat p b
have rw : padicValNat p b - padicValNat p m = padicValNat p b
Tactic: rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
    Nat.sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
rw : padicValNat p b - padicValNat p m = padicValNat p b
⊢ padicValNat p (b / m) = padicValNat p b
have rw₁ : padicValNat p b - 0 = padicValNat p b
Tactic: rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
    Nat.sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : p.Coprime m
b : ℕ
dvd : m ∣ b
rw : padicValNat p b - padicValNat p m = padicValNat p b
rw₁ : padicValNat p b - 0 = padicValNat p b
⊢ padicValNat p (b / m) = padicValNat p b
have rw₂ : padicValNat p b = padicValNat p b
Tactic: rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
    Nat.sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : 1 ≤ padicValNat p n
⊢ p ∣ n
have by_contra : ∀ (h : ¬p ∣ n), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ False
have hp₁ : LE.le (α := ℕ) 1 0
Tactic: rw [padicValNat.eq_zero_of_not_dvd h] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
a n : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a
have rw : (↑n : ℕ∞) ≤ emultiplicity p a ↔ n ≤ padicValNat p a
Tactic: rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity_of_ne_one hp ha, Nat.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
a n : ℕ
ha : a ≠ 0
rw : (↑n : ℕ∞) ≤ emultiplicity p a ↔ n ≤ padicValNat p a
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a
have rw₁ : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(padicValNat p a) : ℕ∞) ↔ n ≤ padicValNat p a
Tactic: rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity_of_ne_one hp ha, Nat.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
a n : ℕ
ha : a ≠ 0
rw : (↑n : ℕ∞) ≤ emultiplicity p a ↔ n ≤ padicValNat p a
rw₁ : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(padicValNat p a) : ℕ∞) ↔ n ≤ padicValNat p a
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a
have rw₂ : n ≤ padicValNat p a ↔ n ≤ padicValNat p a
Tactic: rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity_of_ne_one hp ha, Nat.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
n a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
have inl : p ^ n ∣ 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ padicValNat p 0
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
n a : ℕ
inl : p ^ n ∣ 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ padicValNat p 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
have inr : ∀ (ha : a ≠ 0), p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
have inr : n ≤ padicValNat p a ↔ a = 0 ∨ n ≤ padicValNat p a
Tactic: rw [padicValNat_dvd_iff_le_of_ne_one hp ha, or_iff_right ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
inr : n ≤ padicValNat p a ↔ a = 0 ∨ n ≤ padicValNat p a
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
have inr₁ : n ≤ padicValNat p a ↔ n ≤ padicValNat p a
Tactic: rw [padicValNat_dvd_iff_le_of_ne_one hp ha, or_iff_right ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ ¬p ^ (padicValNat p n + 1) ∣ n
have rw : padicValNat p n < padicValNat p n + 1
Tactic: rw [padicValNat_dvd_iff_le hn, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
ne : p ≠ q
⊢ padicValNat p (q ^ n) = 0
have rw : n * padicValNat p q = 0
Tactic: rw [padicValNat.pow _ <| Nat.Prime.ne_zero hq.elim, padicValNat_primes ne, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
ne : p ≠ q
rw : n * padicValNat p q = 0
⊢ padicValNat p (q ^ n) = 0
have rw₁ : n * 0 = 0
Tactic: rw [padicValNat.pow _ <| Nat.Prime.ne_zero hq.elim, padicValNat_primes ne, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
ne : p ≠ q
rw : n * padicValNat p q = 0
rw₁ : n * 0 = 0
⊢ padicValNat p (q ^ n) = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [padicValNat.pow _ <| Nat.Prime.ne_zero hq.elim, padicValNat_primes ne, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : p ≠ q
⊢ padicValNat p (p ^ n * q ^ m) = n
have rw : padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
Tactic: rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm,
    padicValNat.prime_pow, padicValNat_prime_prime_pow m ne, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : p ≠ q
rw : padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
⊢ padicValNat p (p ^ n * q ^ m) = n
have rw₁ : n + padicValNat p (q ^ m) = n
Tactic: rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm,
    padicValNat.prime_pow, padicValNat_prime_prime_pow m ne, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : p ≠ q
rw : padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
rw₁ : n + padicValNat p (q ^ m) = n
⊢ padicValNat p (p ^ n * q ^ m) = n
have rw₂ : n + 0 = n
Tactic: rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm,
    padicValNat.prime_pow, padicValNat_prime_prime_pow m ne, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : p ≠ q
rw : padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
rw₁ : n + padicValNat p (q ^ m) = n
rw₂ : n + 0 = n
⊢ padicValNat p (p ^ n * q ^ m) = n
have rw₃ : n = n
Tactic: rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm,
    padicValNat.prime_pow, padicValNat_prime_prime_pow m ne, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (p ^ n * q ^ m) = m
have rw : padicValNat q (q ^ m * p ^ n) = m
Tactic: rw [mul_comm (p ^ n) (q ^ m)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
⊢ padicValNat p n ≤ log p n
have zero : padicValNat p 0 ≤ log p 0
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
zero : padicValNat p 0 ≤ log p 0
⊢ padicValNat p n ≤ log p n
have succ : ∀ (n : ℕ), padicValNat p (n + 1) ≤ log p (n + 1)
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
⊢ padicValNat p (n + 1) ≤ log p (n + 1)
have succ : padicValNat 0 (n + 1) ≤ log 0 (n + 1)
Tactic: rcases p with _ | _ | p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
succ : padicValNat 0 (n + 1) ≤ log 0 (n + 1)
⊢ padicValNat p (n + 1) ≤ log p (n + 1)
have succ₁ : padicValNat (HAdd.hAdd (α := ℕ) 0 1) (n + 1) ≤ log (HAdd.hAdd (α := ℕ) 0 1) (n + 1)
Tactic: rcases p with _ | _ | p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
succ : padicValNat 0 (n + 1) ≤ log 0 (n + 1)
succ₁ : padicValNat (HAdd.hAdd (α := ℕ) 0 1) (n + 1) ≤ log (HAdd.hAdd (α := ℕ) 0 1) (n + 1)
⊢ padicValNat p (n + 1) ≤ log p (n + 1)
have succ₂ : ∀ (p : ℕ), padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)
Tactic: rcases p with _ | _ | p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
⊢ padicValNat p a + p ≤ a
have pos : ∀ (dvd : p ∣ a), padicValNat p a + p ≤ a
Tactic: by_cases dvd : p ∣ a
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
pos : ∀ (dvd : p ∣ a), padicValNat p a + p ≤ a
⊢ padicValNat p a + p ≤ a
have neg : ∀ (dvd : ¬p ∣ a), padicValNat p a + p ≤ a
Tactic: by_cases dvd : p ∣ a
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : p ∣ a
⊢ padicValNat p a + p ≤ a
have pos : ∀ (k : ℕ) (hk : a = p * k), padicValNat p a + p ≤ a
Tactic: rcases dvd with ⟨k, hk⟩
Cleared hypotheses: dvd
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ padicValNat p a + p ≤ a
have this : padicValNat p k < k
Tactic: have : padicValNat p k < k := by calc
      _ ≤ log p k := padicValNat_le_nat_log k
      _ < _ := log_lt_self p (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ padicValNat p a + p ≤ a
have pos : 1 + padicValNat p k + p ≤ p * k
Tactic: rw [hk, padicValNat.mul (by lia) (by lia), padicValNat_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ 1 + padicValNat p k + p ≤ p * k
have _ : 1 + padicValNat p k + p ≤ p + k
Tactic: calc
      _ ≤ p + k := by lia
      _ ≤ _ := Nat.add_le_mul hp.out.two_le (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a
have neg : 0 + p ≤ a
Tactic: rw [padicValNat.eq_zero_of_not_dvd dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)
have rw : n < p ^ (padicValNat p n + 1) → p ^ padicValNat p n ≤ n
Tactic: rw [Nat.log_eq_iff (Or.inr ⟨(Nat.Prime.one_lt' p).out, by lia⟩), and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ log 2 n ≠ padicValNat 2 (n + 1)
have rw : ¬(HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) ≤ n ∧ n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1))
Tactic: rw [Ne, log_eq_iff (by simp [hn])]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) ≤ n
h2 : n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1)
⊢ False
have h1₁ : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
Tactic: rw [← Nat.lt_add_one_iff, ← mul_one (2 ^ _)] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n < HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1) + 1)
⊢ False
have h2₁ : n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2
Tactic: rw [← add_one_le_iff, Nat.pow_succ] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
h1 : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 1 < n + 1
h2 : n + 1 ≤ HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * 2
⊢ False
have refine : HPow.hPow (α := ℕ) 2 (padicValNat 2 (n + 1)) * HAdd.hAdd (α := ℕ) 1 1 ≠ n + 1
Tactic: refine not_dvd_of_lt_of_lt_mul_succ h1 (lt_of_le_of_ne' h2 ?_) pow_padicValNat_dvd
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Prime p)
⊢ max (log p n) (padicValNat p (n + 1)) = log p (n + 1)
have apply : log p (n + 1) ≤ max (log p n) (padicValNat p (n + 1))
Tactic: apply le_antisymm (max_le (le_log_of_pow_le hp.out.one_lt (pow_log_le_add_one p n))
    (padicValNat_le_nat_log (n + 1)))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Prime p)
⊢ log p (n + 1) ≤ max (log p n) (padicValNat p (n + 1))
have rw : log p n < log p (n + 1) → log p (n + 1) ≤ padicValNat p (n + 1)
Tactic: rw [le_max_iff, or_iff_not_imp_left, not_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p n : ℕ
hp : Fact (Prime p)
h : log p n < log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)
have h₁ : n + 1 = p ^ log p (n + 1)
Tactic: replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt hp.out.one_lt h))
    (pow_log_le_self p n.succ_ne_zero)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Prime p)
h : n + 1 = p ^ log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)
have rw : log p (p ^ log p (n + 1)) ≤ padicValNat p (p ^ log p (n + 1))
Tactic: rw [h, padicValNat.prime_pow, ← h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Prime p)
h : n + 1 = p ^ log p (n + 1)
rw : log p (p ^ log p (n + 1)) ≤ padicValNat p (p ^ log p (n + 1))
⊢ log p (n + 1) ≤ padicValNat p (n + 1)
have rw₁ : log p (p ^ log p (n + 1)) ≤ log p (n + 1)
Tactic: rw [h, padicValNat.prime_pow, ← h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Prime p)
h : n + 1 = p ^ log p (n + 1)
rw : log p (p ^ log p (n + 1)) ≤ padicValNat p (p ^ log p (n + 1))
rw₁ : log p (p ^ log p (n + 1)) ≤ log p (n + 1)
⊢ log p (n + 1) ≤ padicValNat p (n + 1)
have rw₂ : log p (n + 1) ≤ log p (n + 1)
Tactic: rw [h, padicValNat.prime_pow, ← h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : Membership.mem (γ := Finset ℕ) (Finset.image (fun (x : ℕ) ↦ p ^ x) (Finset.range (padicValNat p n + 1))) t
⊢ t ∈ n.divisors
have ht₁ : ∃ a < padicValNat p n + 1, p ^ a = t
Tactic: simp only [Finset.mem_image, Finset.mem_range] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n + 1, p ^ a = t
⊢ t ∈ n.divisors
have obtain : ∀ (k : ℕ) (hk : k < padicValNat p n + 1), p ^ k ∈ n.divisors
Tactic: obtain ⟨k, hk, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ n.divisors
have rw : p ^ k ∣ n ∧ n ≠ 0
Tactic: rw [Nat.mem_divisors]