awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
⊢ 0 < min (padicValRat p (∑ x ∈ Finset.range d, F x)) (padicValRat p (F d))

Tactic:
lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))

Premises used: lt_add_one, lt_min
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
neg : ∀ (i : ℕ) (hi : i < d), 0 < padicValRat p (F i)
⊢ 0 < min (padicValRat p (∑ x ∈ Finset.range d, F x)) (padicValRat p (F d))

Tactic:
refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))

Premises used: lt_add_one, lt_min
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)

Tactic:
hF _ (lt_trans hi (lt_add_one _))

Premises used: lt_add_one, lt_trans
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd :
  ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬Eq (α := ℚ) (∑ x ∈ Finset.range d, F x) 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)

Tactic:
exact hF _ (lt_trans hi (lt_add_one _))

Premises used: lt_add_one, lt_trans
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ i < n, 0 < padicValRat p (F i)
hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range n, F i) 0
zero :
  ∀ (hF : ∀ i < 0, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range 0, F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range 0, F i)
succ :
  ∀ (d : ℕ)
    (hd :
      ∀ (hF : ∀ i < d, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range d, F i) 0),
        0 < padicValRat p (∑ i ∈ Finset.range d, F i))
    (hF : ∀ i < d + 1, 0 < padicValRat p (F i)) (hn0 : Ne (α := ℚ) (∑ i ∈ Finset.range (d + 1), F i) 0),
    0 < padicValRat p (∑ i ∈ Finset.range (d + 1), F i)
⊢ 0 < padicValRat p (∑ i ∈ Finset.range n, F i)

Tactic:
induction n with
  | zero => exact False.elim (hn0 rfl)
  | succ d hd =>
    rw [Finset.sum_range_succ] at hn0 ⊢
    by_cases h : ∑ x ∈ Finset.range d, F x = 0
    · rw [h, zero_add]
      exact hF d (lt_add_one _)
    · refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
      refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
      exact hF _ (lt_trans hi (lt_add_one _))

Premises used: padicValRat.min_le_padicValRat_add, False.elim, zero_add, Nat.zero, Nat.succ, Finset.sum_range_succ, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
k : ℕ
hF : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) {k} i → padicValRat p (F j) < padicValRat p (F i)
singleton : padicValRat p (F j) < padicValRat p (F k)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ {k}, F i)

Tactic:
rw [Finset.sum_singleton]

Premises used: Finset.sum_singleton
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
k : ℕ
hF : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) {k} i → padicValRat p (F j) < padicValRat p (F i)
⊢ Membership.mem (γ := Finset ℕ) {k} k

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
k : ℕ
hF : ∀ (i : ℕ), Membership.mem (γ := Finset ℕ) {k} i → padicValRat p (F j) < padicValRat p (F i)
⊢ padicValRat p (F j) < padicValRat p (F k)

Tactic:
exact hF k (by simp)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
cons : padicValRat p (F j) < padicValRat p (F s + ∑ x ∈ S', F x)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ Finset.cons s S' Hnot, F i)

Tactic:
rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]

Premises used: Finset.cons_eq_insert, Finset.sum_insert
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
⊢ s ∈ Finset.cons s S' Hnot

Tactic:
simp [Finset.mem_insert, true_or]

Premises used: true_or, Finset.mem_insert
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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'
rw : i = s ∨ i ∈ S'
⊢ i ∈ Finset.cons s S' Hnot

Tactic:
rw [Finset.cons_eq_insert, Finset.mem_insert]

Premises used: Finset.mem_insert, Finset.cons_eq_insert
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 = s ∨ i ∈ S'

Tactic:
Or.inr hi

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 = s ∨ i ∈ S'

Tactic:
exact Or.inr hi

Premises used: Or.inr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
⊢ padicValRat p (F j) < padicValRat p (F s + ∑ x ∈ S', F x)

Tactic:
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)))

Premises used: add_pos, Finset.sum_pos, ne_of_gt, padicValRat.lt_add_of_lt
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
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)
⊢ padicValRat p (F j) < padicValRat p (∑ i ∈ S, 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)))

Premises used: Finset.sum_singleton, Finset.cons_eq_insert, Singleton.singleton
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
⊢ a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b

Tactic:
mod_cast padicValRat.mul (p := p) (q := a) (r := b)

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, Nat.cast_add._simp_1, cast, padicValNat, Ne, padicValRat, Nat.cast, padicValRat_of_nat._simp_1, HAdd.hAdd, implies_congr, congr, Eq.refl, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
inr : ∀ (ha : a ≠ 0), padicValNat p (a / b) = padicValNat p a - padicValNat p b
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
inr : ∀ (k : ℕ) (ha : b * k ≠ 0), padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b

Tactic:
obtain ⟨k, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ b ≠ 0

Tactic:
obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
⊢ k ≠ 0

Tactic:
obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha

Premises used: Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
inr₃ inr₄ : padicValNat p k = padicValNat p k
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b

Tactic:
rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]

Premises used: Nat.mul_div_cancel, padicValNat.mul, mul_comm, Nat.add_sub_cancel, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
rw : padicValNat p b - padicValNat p p = padicValNat p b - 1
rw₁ rw₂ : padicValNat p b - 1 = padicValNat p b - 1
⊢ padicValNat p (b / p) = padicValNat p b - 1

Tactic:
rw [padicValNat.div_of_dvd dvd, padicValNat_self]

Premises used: padicValNat_self, padicValNat.div_of_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ha : a ≠ 0
⊢ padicValNat p (a ^ n) = n * padicValNat p a

Tactic:
simpa only [← @Nat.cast_inj ℤ, push_cast] using padicValRat.pow (Nat.cast_ne_zero.mpr ha)

Premises used: Iff.mpr, Nat.cast_inj, padicValRat.pow, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : n * padicValNat p p = n
rw₁ : n * 1 = n
rw₂ rw₃ : n = n
⊢ padicValNat p (p ^ n) = n

Tactic:
rw [padicValNat.pow _ (@Fact.out p.Prime).ne_zero, padicValNat_self, mul_one]

Premises used: padicValNat.pow, padicValNat_self, Nat.Prime.ne_zero, mul_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₁ rw₂ : padicValNat p b - a = padicValNat p b - a
⊢ padicValNat p (b / p ^ a) = padicValNat p b - a

Tactic:
rw [padicValNat.div_of_dvd dvd, padicValNat.prime_pow]

Premises used: padicValNat.prime_pow, padicValNat.div_of_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₂ rw₃ : padicValNat p b = padicValNat p b
⊢ padicValNat p (b / 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]

Premises used: padicValNat.div_of_dvd, Iff.mp, Nat.sub_zero, padicValNat.eq_zero_of_not_dvd, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : 1 ≤ padicValNat p n
by_contra : ∀ (h : ¬p ∣ n), False
⊢ p ∣ n

Tactic:
by_contra h
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
⊢ LE.le (α := ℕ) 1 0

Tactic:
rw [padicValNat.eq_zero_of_not_dvd h] at hp

Premises used: padicValNat.eq_zero_of_not_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : 1 ≤ padicValNat p n
h : ¬p ∣ n
hp₁ : LE.le (α := ℕ) 1 0
⊢ ¬p ∣ n

Tactic:
rw [padicValNat.eq_zero_of_not_dvd h] at hp

Premises used: padicValNat.eq_zero_of_not_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : LE.le (α := ℕ) 1 0
h : ¬p ∣ n
⊢ False

Tactic:
lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)

Premises used: lt_irrefl, zero_lt_one, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : LE.le (α := ℕ) 1 0
h : ¬p ∣ n
⊢ False

Tactic:
exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)

Premises used: lt_irrefl, zero_lt_one, OfNat.ofNat, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₂ rw₃ : n ≤ padicValNat p a ↔ n ≤ padicValNat p a
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a

Tactic:
rw [pow_dvd_iff_le_emultiplicity, ← padicValNat_eq_emultiplicity_of_ne_one hp ha, Nat.cast_le]

Premises used: pow_dvd_iff_le_emultiplicity, padicValNat_eq_emultiplicity_of_ne_one, Nat.cast_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a n : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ n ≤ padicValNat p a

Tactic:
padicValNat_dvd_iff_le_of_ne_one hp.out.ne_one ha

Premises used: Nat.Prime.ne_one, padicValNat_dvd_iff_le_of_ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : p ≠ 1
n a : ℕ
inl : p ^ n ∣ 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ padicValNat p 0
inr : ∀ (ha : a ≠ 0), p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
⊢ p ^ n ∣ 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ padicValNat p 0

Tactic:
iff_of_true (dvd_zero _) (Or.inl rfl)

Premises used: dvd_zero, iff_of_true, Or.inl, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : p ≠ 1
n : ℕ
⊢ p ^ n ∣ 0 ↔ Eq (α := ℕ) 0 0 ∨ n ≤ padicValNat p 0

Tactic:
exact iff_of_true (dvd_zero _) (Or.inl rfl)

Premises used: dvd_zero, iff_of_true, Or.inl, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : p ≠ 1
n a : ℕ
ha : a ≠ 0
inr : n ≤ padicValNat p a ↔ a = 0 ∨ n ≤ padicValNat p a
inr₁ inr₂ : n ≤ padicValNat p a ↔ n ≤ padicValNat p a
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
rw [padicValNat_dvd_iff_le_of_ne_one hp ha, or_iff_right ha]

Premises used: padicValNat_dvd_iff_le_of_ne_one, or_iff_right
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
padicValNat_dvd_iff_of_ne_one hp.out.ne_one n a

Premises used: padicValNat_dvd_iff_of_ne_one, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
rw : padicValNat p n < padicValNat p n + 1
⊢ ¬p ^ (padicValNat p n + 1) ∣ n

Tactic:
rw [padicValNat_dvd_iff_le hn, not_le]

Premises used: not_le, padicValNat_dvd_iff_le
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1

Tactic:
exact Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
ne : p ≠ q
⊢ padicValNat p q = 0

Tactic:
@padicValNat.eq_zero_of_not_dvd p q <|
    (not_congr (Iff.symm (prime_dvd_prime_iff_eq hp.1 hq.1))).mp ne

Premises used: Nat.prime_dvd_prime_iff_eq, Iff.mp, padicValNat.eq_zero_of_not_dvd, Iff.symm, not_congr, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ padicValNat p (q ^ n) = 0

Tactic:
rw [padicValNat.pow _ <| Nat.Prime.ne_zero hq.elim, padicValNat_primes ne, mul_zero]

Premises used: padicValNat.pow, MulZeroClass.mul_zero, padicValNat_primes, Fact.elim, Nat.Prime.ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₃ rw₄ : n = n
⊢ padicValNat p (p ^ n * 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]

Premises used: NeZero.ne', padicValNat_prime_prime_pow, Ne.symm, padicValNat.prime_pow, HPow.hPow, padicValNat.mul, add_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
rw : padicValNat q (q ^ m * p ^ n) = m
⊢ padicValNat q (p ^ n * q ^ m) = m

Tactic:
rw [mul_comm (p ^ n) (q ^ m)]

Premises used: HPow.hPow, mul_comm
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (q ^ m * p ^ n) = m

Tactic:
padicValNat_mul_pow_left m n ne

Premises used: padicValNat_mul_pow_left
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (q ^ m * p ^ n) = m

Tactic:
exact padicValNat_mul_pow_left m n ne

Premises used: padicValNat_mul_pow_left
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
zero : padicValNat p 0 ≤ log p 0
succ : ∀ (n : ℕ), padicValNat p (n + 1) ≤ log p (n + 1)
⊢ padicValNat p n ≤ log p n

Tactic:
rcases n with _ | n
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
⊢ padicValNat p 0 ≤ log p 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)
succ₂ : ∀ (p : ℕ), padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)
⊢ padicValNat p (n + 1) ≤ log p (n + 1)

Tactic:
rcases p with _ | _ | p
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
⊢ padicValNat 0 (n + 1) ≤ log 0 (n + 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n : ℕ
⊢ padicValNat (HAdd.hAdd (α := ℕ) 0 1) (n + 1) ≤ log (HAdd.hAdd (α := ℕ) 0 1) (n + 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)

Tactic:
Nat.le_log_of_pow_le p.one_lt_succ_succ (le_of_dvd n.succ_pos pow_padicValNat_dvd)

Premises used: Nat.one_lt_succ_succ, Nat.le_log_of_pow_le, pow_padicValNat_dvd, Nat.succ_pos, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
n p : ℕ
⊢ padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)

Tactic:
exact Nat.le_log_of_pow_le p.one_lt_succ_succ (le_of_dvd n.succ_pos pow_padicValNat_dvd)

Premises used: Nat.one_lt_succ_succ, Nat.le_log_of_pow_le, pow_padicValNat_dvd, Nat.succ_pos, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
pos : ∀ (dvd : p ∣ a), padicValNat p a + p ≤ a
neg : ∀ (dvd : ¬p ∣ a), padicValNat p a + p ≤ a
⊢ padicValNat p a + p ≤ a

Tactic:
by_cases dvd : p ∣ a
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : p ∣ a
pos : ∀ (k : ℕ) (hk : a = p * k), padicValNat p a + p ≤ a
⊢ padicValNat p a + p ≤ a

Tactic:
rcases dvd with ⟨k, hk⟩
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ padicValNat p k ≤ log p k

Tactic:
padicValNat_le_nat_log k

Premises used: padicValNat_le_nat_log
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ padicValNat p k < k

Tactic:
calc
      _ ≤ log p k := padicValNat_le_nat_log k
      _ < _ := log_lt_self p (by lia)

Premises used: Nat.log_lt_self, Nat.log, padicValNat_le_nat_log
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ 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)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ p ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
pos : 1 + padicValNat p k + p ≤ p * k
⊢ padicValNat p a + p ≤ a

Tactic:
rw [hk, padicValNat.mul (by lia) (by lia), padicValNat_self]

Premises used: padicValNat_self, padicValNat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
this : padicValNat p k < k
⊢ 2 ≤ k

Tactic:
lia