awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
simp : clog b (n + 1) ≤ clog b n → clog b n ≤ clog b (n + 1)
⊢ clog b n = clog b (n + 1) ↔ clog b (n + 1) ≤ clog b n

Tactic:
simp only [le_antisymm_iff, and_iff_right_iff_imp]

Premises used: le_antisymm_iff, and_iff_right_iff_imp
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
⊢ clog b (n + 1) ≤ clog b n → clog b n ≤ clog b (n + 1)

Tactic:
fun _ ↦ clog_monotone b (le_add_right n 1)

Premises used: Nat.le_add_right, Nat.clog_monotone, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : 1 < b
⊢ clog b (n + 1) ≤ clog b n → clog b n ≤ clog b (n + 1)

Tactic:
exact fun _ ↦ clog_monotone b (le_add_right n 1)

Premises used: Nat.le_add_right, Nat.clog_monotone, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
inl : clog (HPow.hPow (β := ℕ) b 0) n = (clog b n + HSub.hSub (α := ℕ) 0 1) / 0
inr : ∀ (hk : k > 0), clog (b ^ k) n = (clog b n + (k - 1)) / k
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
⊢ clog (HPow.hPow (β := ℕ) b 0) n = (clog b n + HSub.hSub (α := ℕ) 0 1) / 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
inr : ∀ (hb : 1 < b), clog (b ^ k) n = (clog b n + (k - 1)) / k
inr₁ : ∀ (hb : 1 ≥ b), clog (b ^ k) n = (clog b n + (k - 1)) / k
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb

Premises used: Nat.lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
eq_of_forall_lt_iff fun c ↦ ?_

Premises used: eq_of_forall_lt_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
inr : ∀ (c : ℕ), c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
refine eq_of_forall_lt_iff fun c ↦ ?_

Premises used: eq_of_forall_lt_iff
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 < b
c : ℕ
inr : (b ^ k) ^ c < n ↔ c < (clog b n + (k - 1)) / k
inr₁ : (b ^ k) ^ c < n ↔ c * k < clog b n + (k - 1) - (k - 1)
inr₂ : (b ^ k) ^ c < n ↔ c * k < clog b n
inr₃ : (b ^ k) ^ c < n ↔ b ^ (c * k) < n
inr₄ inr₅ : (b ^ k) ^ c < n ↔ (b ^ k) ^ c < n
⊢ c < clog (b ^ k) n ↔ c < (clog b n + (k - 1)) / k

Tactic:
rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']

Premises used: Nat.one_lt_pow, Nat.lt_clog_iff_pow_lt, Nat.lt_div_iff_mul_lt, Nat.add_sub_cancel, Nat.pow_mul', Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
this : (k - 1) / k = 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
grind [clog_of_left_le_one, Nat.pow_le_one_iff]

Premises used: Nat.pow_le_one_iff, Nat.clog_of_left_le_one
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
inr : (k - 1) / k = 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
inr : k - 1 < k
⊢ (k - 1) / k = 0

Tactic:
apply Nat.div_eq_of_lt

Premises used: Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Log
Goal:
b k n : ℕ
hk : k > 0
hb : 1 ≥ b
⊢ k - 1 < k

Tactic:
grind
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p_1 n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ 1 < p * p ∧ n ≠ 0

Tactic:
simp [Nat.one_lt_mul_iff, hp, Nat.lt_trans Nat.one_pos]

Premises used: Nat.one_pos, Nat.one_lt_mul_iff, Nat.lt_trans
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ p ∣ n

Tactic:
rw [← Nat.dvd_iff_mod_eq_zero] at hmod

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : p ∣ n
rcases : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0), p * m / (p * p) < p * m / p
⊢ n / (p * p) < n / p

Tactic:
rcases hmod with ⟨m, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p m : ℕ
hp : 1 < p ∧ p * m ≠ 0
⊢ 0 < p

Tactic:
have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p m : ℕ
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
rw : m / p < m
⊢ p * m / (p * p) < p * m / p

Tactic:
rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]

Premises used: Nat.mul_div_cancel_left, Nat.mul_div_mul_left
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p m : ℕ
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ 0 < m

Tactic:
grind
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p m : ℕ
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ m / p < m

Tactic:
exact Nat.div_lt_self (by grind) hp.1

Premises used: Nat.div_lt_self, And.left
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
rw rw₁ rw₂ : ∀ (hmod : p ∣ n), n / (p * p) < n / p
rw₃ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0), p * m / (p * p) < p * m / p
rw₄ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0) (hp₀ : 0 < p), p * m / (p * p) < p * m / p
rw₅ : ∀ (m : ℕ) (hp : 1 < p ∧ p * m ≠ 0) (hp₀ : 0 < p), m / p < m
⊢ n / (p * p) < n / p

Tactic:
decreasing_by
    rw [← Nat.dvd_iff_mod_eq_zero] at hmod
    rcases hmod with ⟨m, rfl⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    rw [Nat.mul_div_mul_left _ _ hp₀, Nat.mul_div_cancel_left _ hp₀]
    exact Nat.div_lt_self (by grind) hp.1

Premises used: Nat.div_lt_self, And.left, Nat.dvd_iff_mod_eq_zero, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd

Tactic:
rw [heq] at ih
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
case1 :
  ∀ (hdvd : ¬p * p ∣ (e, q).snd) (hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0)
    (hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0)
    (heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)),
    (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧
      ¬p ∣ (2 * e + 1, q / p).snd
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
rcases ih with ⟨rfl, hdvd⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p_1 p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ 0 < p

Tactic:
have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p_1 p e q : ℕ
hqp : q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
hp₀ : 0 < p
⊢ (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e + 1, q / p).snd

Tactic:
simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]

Premises used: Nat.div_mul_cancel, Nat.mul_assoc, Nat.mul_pow, Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.pow_add'
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd

Tactic:
rw [heq] at ih
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p_1 p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (e, q).snd * (p * p) ^ (e, q).fst = n ∧ ¬p * p ∣ (e, q).snd
case2 :
  ∀ (hdvd : ¬p * p ∣ (e, q).snd) (hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0)
    (hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0)
    (heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)),
    (2 * e, q).snd * p ^ (2 * e, q).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e, q).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd

Tactic:
rcases ih with ⟨rfl, hdvd⟩

Premises used: rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p_1 p e q : ℕ
hqp : ¬q % p = 0
hdvd : ¬p * p ∣ (e, q).snd
hp : 1 < p ∧ (e, q).snd * (p * p) ^ (e, q).fst ≠ 0
hmod : (e, q).snd * (p * p) ^ (e, q).fst % p = 0
heq : go ((e, q).snd * (p * p) ^ (e, q).fst) (p * p) ⋯ = (e, q)
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = (e, q).snd * (p * p) ^ (e, q).fst ∧ ¬p ∣ (2 * e, q).snd

Tactic:
simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]

Premises used: Nat.pow_add, Nat.mul_pow, Nat.dvd_iff_mod_eq_zero, Nat.two_mul
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p p_1 : ℕ
hp : 1 < p_1 ∧ n ≠ 0
h : ¬n % p_1 = 0
⊢ Prod.snd (α := ℕ) (0, n) * HPow.hPow (β := ℕ) p_1 (Prod.fst (0, n)) = n ∧ ¬p_1 ∣ Prod.snd (α := ℕ) (0, n)

Tactic:
simp_all [Nat.dvd_iff_mod_eq_zero]

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n p : ℕ
hnp : 1 < p ∧ n ≠ 0
case1 :
  ∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0) (hmod : n % p = 0) (e q : ℕ) (heq : go n (p * p) ⋯ = (e, q)) (hqp : q % p = 0)
    (ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd),
    (2 * e + 1, q / p).snd * p ^ (2 * e + 1, q / p).fst = n ∧ ¬p ∣ (2 * e + 1, q / p).snd
case2 :
  ∀ (p : ℕ) (hp : 1 < p ∧ n ≠ 0) (hmod : n % p = 0) (e q : ℕ) (heq : go n (p * p) ⋯ = (e, q)) (hqp : ¬q % p = 0)
    (ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd),
    (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd
case3 :
  ∀ (p : ℕ),
    1 < p ∧ n ≠ 0 →
      ¬n % p = 0 → Prod.snd (α := ℕ) (0, n) * HPow.hPow (β := ℕ) p (Prod.fst (0, n)) = n ∧ ¬p ∣ Prod.snd (α := ℕ) (0, n)
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd

Tactic:
fun_induction go with
  | case1 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    have hp₀ : 0 < p := Nat.lt_trans Nat.one_pos hp.1
    simp_all [← Nat.dvd_iff_mod_eq_zero, Nat.pow_add', ← Nat.mul_assoc, Nat.div_mul_cancel,
      Nat.two_mul, Nat.mul_pow]
  | case2 p hp hmod e q heq hqp ih =>
    rw [heq] at ih
    rcases ih with ⟨rfl, hdvd⟩
    simp_all [Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.mul_pow, Nat.pow_add]
  | case3 =>
    simp_all [Nat.dvd_iff_mod_eq_zero]

Premises used: Nat.pow_add, Nat.div_mul_cancel, Nat.mul_assoc, Nat.mul_pow, Nat.dvd_iff_mod_eq_zero, Nat.two_mul, Nat.pow_add', rfl, Nat.maxPowDvdDiv.go
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≤ 1
n : ℕ
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
simp [maxPowDvdDiv, Nat.not_lt_of_ge hp]

Premises used: Nat.maxPowDvdDiv, Nat.not_lt_of_ge
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
⊢ maxPowDvdDiv 0 n = (0, n)

Tactic:
maxPowDvdDiv_of_base_le_one (Nat.zero_le _) _

Premises used: Nat.zero_le, Nat.maxPowDvdDiv_of_base_le_one
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
⊢ padicValNat 0 n = 0

Tactic:
simp [padicValNat]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
⊢ n.divMaxPow 0 = n

Tactic:
simp [divMaxPow]

Premises used: Nat.divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
⊢ maxPowDvdDiv 1 n = (0, n)

Tactic:
maxPowDvdDiv_of_base_le_one (Nat.le_refl _) _

Premises used: Nat.le_refl, Nat.maxPowDvdDiv_of_base_le_one
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
⊢ padicValNat 1 n = 0

Tactic:
simp [padicValNat]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
⊢ n.divMaxPow 1 = n

Tactic:
simp [divMaxPow]

Premises used: Nat.divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
⊢ p.maxPowDvdDiv 0 = (0, 0)

Tactic:
simp [maxPowDvdDiv]

Premises used: Nat.maxPowDvdDiv
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
⊢ padicValNat p 0 = 0

Tactic:
simp [padicValNat]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
⊢ divMaxPow 0 p = 0

Tactic:
simp [divMaxPow]

Premises used: Nat.divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
h : ¬p ∣ 0
⊢ p.maxPowDvdDiv 0 = (0, 0)

Tactic:
simp at h
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
h : ¬p ∣ n + 1
⊢ p.maxPowDvdDiv (n + 1) = (0, n + 1)

Tactic:
simp [maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero.not.mp h, maxPowDvdDiv.go]

Premises used: Iff.not, Nat.maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero, Iff.mp, Nat.maxPowDvdDiv.go
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
h : ¬p ∣ n
zero : ∀ (h : ¬p ∣ 0), p.maxPowDvdDiv 0 = (0, 0)
succ : ∀ (n : ℕ) (h : ¬p ∣ n + 1), p.maxPowDvdDiv (n + 1) = (0, n + 1)
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
cases n with
  | zero => simp at h
  | succ n => simp [maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero.not.mp h, maxPowDvdDiv.go]

Premises used: Iff.not, Nat.maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero, Iff.mp, Nat.zero, Nat.succ, Nat.maxPowDvdDiv.go
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
inl : maxPowDvdDiv 1 1 = (0, 1)
inr : ∀ (hp : p ≠ 1), p.maxPowDvdDiv 1 = (0, 1)
⊢ p.maxPowDvdDiv 1 = (0, 1)

Tactic:
rcases eq_or_ne p 1 with rfl | hp

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
⊢ maxPowDvdDiv 1 1 = (0, 1)

Tactic:
simp [maxPowDvdDiv_of_not_dvd, *]

Premises used: Nat.maxPowDvdDiv_of_not_dvd
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
hp : p ≠ 1
⊢ p.maxPowDvdDiv 1 = (0, 1)

Tactic:
simp [maxPowDvdDiv_of_not_dvd, *]

Premises used: Nat.maxPowDvdDiv_of_not_dvd
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
⊢ padicValNat p 1 = 0

Tactic:
simp [padicValNat]

Premises used: padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p : ℕ
⊢ divMaxPow 1 p = 1

Tactic:
simp [divMaxPow]

Premises used: Nat.divMaxPow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
h : 1 < p ∧ n ≠ 0
⊢ (go n p h).snd * p ^ (go n p h).fst = n

Tactic:
go_spec h |>.1

Premises used: Nat.maxPowDvdDiv.go_spec, And.left
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
h : 1 < p ∧ n ≠ 0
⊢ (go n p h).snd * p ^ (go n p h).fst = n

Tactic:
exact go_spec h |>.1

Premises used: Nat.maxPowDvdDiv.go_spec, And.left
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
h : ¬(1 < p ∧ n ≠ 0)
⊢ Prod.snd (α := ℕ) (0, n) * HPow.hPow (β := ℕ) p (Prod.fst (0, n)) = n

Tactic:
simp
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
case1 : ∀ (h : 1 < p ∧ n ≠ 0), (go n p h).snd * p ^ (go n p h).fst = n
case2 : ∀ (h : ¬(1 < p ∧ n ≠ 0)), Prod.snd (α := ℕ) (0, n) * HPow.hPow (β := ℕ) p (Prod.fst (0, n)) = n
⊢ (p.maxPowDvdDiv n).snd * p ^ (p.maxPowDvdDiv n).fst = n

Tactic:
fun_cases maxPowDvdDiv with
  | case1 h => exact go_spec h |>.1
  | case2 h => simp

Premises used: Nat.maxPowDvdDiv
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
rw : n.divMaxPow p * p ^ padicValNat p n = n
rw₁ rw₂ : n = n
⊢ p ^ padicValNat p n * n.divMaxPow p = n

Tactic:
rw [Nat.mul_comm, divMaxPow_mul_pow_padicValNat]

Premises used: Nat.mul_comm, Nat.divMaxPow_mul_pow_padicValNat
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
⊢ n = p ^ padicValNat p n * n.divMaxPow p

Tactic:
simp
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ ¬p ∣ n.divMaxPow p

Tactic:
simp [divMaxPow, maxPowDvdDiv, maxPowDvdDiv.go_spec, *]

Premises used: Nat.divMaxPow, Nat.maxPowDvdDiv, Nat.maxPowDvdDiv.go_spec
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k n a b : ℕ
hp : 1 < p
hn : n ≠ 0
hab : p ^ a * b = n
hb : ¬p ∣ b
subst : ∀ (hn : p ^ a * b ≠ 0), p ^ k ∣ p ^ a * b ↔ k ≤ a
⊢ p ^ k ∣ n ↔ k ≤ a

Tactic:
subst hab
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hlt : a < k
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)

Premises used: Nat.not_le_of_lt, iff_of_false
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hlt : a < k
inl : ∀ (hdvd : p ^ k ∣ p ^ a * b), False
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)

Premises used: Nat.not_le_of_lt, iff_of_false
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hlt : a < k
hdvd : p ^ k ∣ p ^ a * b
inl : ∀ (l : ℕ) (hlt : a < a + l + 1) (hdvd : p ^ (a + l + 1) ∣ p ^ a * b), False
⊢ False

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
l : ℕ
hlt : a < a + l + 1
hdvd : p ^ (a + l + 1) ∣ p ^ a * b
⊢ p ^ (l + 1) ∣ b

Tactic:
rw [Nat.add_assoc, Nat.pow_add,
      Nat.mul_dvd_mul_iff_left (Nat.pow_pos (Nat.zero_lt_of_lt hp))] at hdvd

Premises used: Nat.pow_add, Nat.zero_lt_of_lt, Nat.mul_dvd_mul_iff_left, Nat.add_assoc, Nat.pow_pos
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
l : ℕ
hlt : a < a + l + 1
hdvd : p ^ (l + 1) ∣ b
⊢ False

Tactic:
hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd

Premises used: Nat.le_add_left, OfNat.ofNat, Nat.dvd_of_pow_dvd
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
l : ℕ
hlt : a < a + l + 1
hdvd : p ^ (l + 1) ∣ b
⊢ False

Tactic:
exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd

Premises used: Nat.le_add_left, OfNat.ofNat, Nat.dvd_of_pow_dvd
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hle : a ≥ k
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle

Premises used: iff_of_true, Nat.dvd_mul_right_of_dvd
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hle : a ≥ k
inr : p ^ k ∣ p ^ a
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a

Tactic:
refine iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle

Premises used: iff_of_true, Nat.dvd_mul_right_of_dvd
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hle : a ≥ k
⊢ p ^ k ∣ p ^ a

Tactic:
Nat.pow_dvd_pow p hle

Premises used: Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hle : a ≥ k
⊢ p ^ k ∣ p ^ a

Tactic:
exact Nat.pow_dvd_pow p hle

Premises used: Nat.pow_dvd_pow
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
⊢ a < k ∨ a ≥ k

Tactic:
cases Nat.lt_or_ge a k with
  | inl hlt =>
    refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt
    rw [Nat.add_assoc, Nat.pow_add,
      Nat.mul_dvd_mul_iff_left (Nat.pow_pos (Nat.zero_lt_of_lt hp))] at hdvd
    exact hb <| Nat.dvd_of_pow_dvd (Nat.le_add_left 1 l) hdvd
  | inr hle =>
    refine iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle
    exact Nat.pow_dvd_pow p hle

Premises used: Nat.pow_add, Nat.zero_lt_of_lt, Nat.mul_dvd_mul_iff_left, Nat.add_assoc, Nat.lt_or_ge, Nat.pow_pos, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ p = 0 ∨ 1 < p

Tactic:
grind
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
inl : ∀ (hp : Ne (α := ℕ) 0 1), HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
inr : ∀ (hp₁ : 1 < p), p ^ k ∣ n ↔ k ≤ padicValNat p n
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
obtain rfl | hp₁ : p = 0 ∨ 1 < p := by grind

Premises used: rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
k n : ℕ
hn : n ≠ 0
hp : Ne (α := ℕ) 0 1
inl : HPow.hPow (α := ℕ) (β := ℕ) 0 0 ∣ n ↔ 0 ≤ padicValNat 0 n
inl₁ : ∀ (hk : k > 0), HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
⊢ HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n : ℕ
hn : n ≠ 0
hp : Ne (α := ℕ) 0 1
⊢ HPow.hPow (α := ℕ) (β := ℕ) 0 0 ∣ n ↔ 0 ≤ padicValNat 0 n

Tactic:
simp [Nat.ne_of_gt, *]

Premises used: Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
k n : ℕ
hn : n ≠ 0
hp : Ne (α := ℕ) 0 1
hk : k > 0
⊢ HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n

Tactic:
simp [Nat.ne_of_gt, *]

Premises used: Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
pow_dvd_iff_le_of_spec hp₁ hn (pow_padicValNat_mul_divMaxPow p n)
      (not_dvd_divMaxPow hp₁ hn)

Premises used: Nat.not_dvd_divMaxPow, Nat.pow_padicValNat_mul_divMaxPow, _private.0.Nat.pow_dvd_iff_le_of_spec
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
exact pow_dvd_iff_le_of_spec hp₁ hn (pow_padicValNat_mul_divMaxPow p n)
      (not_dvd_divMaxPow hp₁ hn)

Premises used: Nat.not_dvd_divMaxPow, Nat.pow_padicValNat_mul_divMaxPow, _private.0.Nat.pow_dvd_iff_le_of_spec
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
⊢ p = 0 ∨ p = 1 ∨ 1 < p

Tactic:
grind
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
inl : ∀ (h : HPow.hPow (α := ℕ) 0 k * l = n) (hl : ¬0 ∣ l), maxPowDvdDiv 0 n = (k, l)
inr : ∀ (h : HPow.hPow (α := ℕ) 1 k * l = n) (hl : ¬1 ∣ l), maxPowDvdDiv 1 n = (k, l)
inr₁ : ∀ (hp : 1 < p), p.maxPowDvdDiv n = (k, l)
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
obtain rfl | rfl | hp : p = 0 ∨ p = 1 ∨ 1 < p := by grind

Premises used: rfl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n k l : ℕ
hn : n ≠ 0
h : HPow.hPow (α := ℕ) 0 k * l = n
hl : ¬0 ∣ l
inl : k = 0 → maxPowDvdDiv 0 n = (k, l)
inl₁ : k > 0 → maxPowDvdDiv 0 n = (k, l)
⊢ maxPowDvdDiv 0 n = (k, l)

Tactic:
cases k.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n k l : ℕ
hn : n ≠ 0
h : HPow.hPow (α := ℕ) 0 k * l = n
hl : ¬0 ∣ l
h_1 : k = 0
⊢ maxPowDvdDiv 0 n = (k, l)

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n k l : ℕ
hn : n ≠ 0
h : HPow.hPow (α := ℕ) 0 k * l = n
hl : ¬0 ∣ l
h_1 : k > 0
⊢ maxPowDvdDiv 0 n = (k, l)

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
n k l : ℕ
hn : n ≠ 0
h : HPow.hPow (α := ℕ) 1 k * l = n
hl : ¬1 ∣ l
⊢ maxPowDvdDiv 1 n = (k, l)

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
h₁ : k ≤ (p.maxPowDvdDiv n).fst
h₂ : (p.maxPowDvdDiv n).fst ≤ k
⊢ k = (p.maxPowDvdDiv n).fst

Tactic:
apply Nat.le_antisymm

Premises used: Nat.le_antisymm
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
h₁ : k ≤ k
⊢ k ≤ (p.maxPowDvdDiv n).fst

Tactic:
rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]

Premises used: padicValNat, Nat.pow_dvd_iff_le_padicValNat, _private.0.Nat.pow_dvd_iff_le_of_spec, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ k

Tactic:
apply Nat.le_refl

Premises used: Nat.le_refl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
h₂ : (p.maxPowDvdDiv n).fst ≤ padicValNat p n
⊢ (p.maxPowDvdDiv n).fst ≤ k

Tactic:
rw [← pow_dvd_iff_le_of_spec hp hn h hl, pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn]

Premises used: Nat.pow_dvd_iff_le_padicValNat, _private.0.Nat.pow_dvd_iff_le_of_spec, Nat.ne_of_gt
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ padicValNat p n

Tactic:
apply Nat.le_refl

Premises used: Nat.le_refl
-- Module: Mathlib.Data.Nat.MaxPowDiv
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k = (p.maxPowDvdDiv n).fst

Tactic:
have hk : k = (p.maxPowDvdDiv n).1 := by
      · apply Nat.le_antisymm
        · rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]
          apply Nat.le_refl
        · rw [← pow_dvd_iff_le_of_spec hp hn h hl, pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn]
          apply Nat.le_refl