awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd
have 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)
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]
Cleared hypotheses: hnp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
h : ¬p ∣ n
⊢ p.maxPowDvdDiv n = (0, n)
have zero : ∀ (h : ¬p ∣ 0), p.maxPowDvdDiv 0 = (0, 0)
Tactic: cases n with
  | zero => simp at h
  | succ n => simp [maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero.not.mp h, maxPowDvdDiv.go]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
h : ¬p ∣ n
zero : ∀ (h : ¬p ∣ 0), p.maxPowDvdDiv 0 = (0, 0)
⊢ p.maxPowDvdDiv n = (0, n)
have succ : ∀ (n : ℕ) (h : ¬p ∣ n + 1), p.maxPowDvdDiv (n + 1) = (0, n + 1)
Tactic: cases n with
  | zero => simp at h
  | succ n => simp [maxPowDvdDiv, Nat.dvd_iff_mod_eq_zero.not.mp h, maxPowDvdDiv.go]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p : ℕ
⊢ p.maxPowDvdDiv 1 = (0, 1)
have inl : maxPowDvdDiv 1 1 = (0, 1)
Tactic: rcases eq_or_ne p 1 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p : ℕ
inl : maxPowDvdDiv 1 1 = (0, 1)
⊢ p.maxPowDvdDiv 1 = (0, 1)
have inr : ∀ (hp : p ≠ 1), p.maxPowDvdDiv 1 = (0, 1)
Tactic: rcases eq_or_ne p 1 with rfl | hp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
⊢ (p.maxPowDvdDiv n).snd * p ^ (p.maxPowDvdDiv n).fst = n
have case1 : ∀ (h : 1 < p ∧ n ≠ 0), (go n p h).snd * p ^ (go n p h).fst = n
Tactic: fun_cases maxPowDvdDiv with
  | case1 h => exact go_spec h |>.1
  | case2 h => simp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
case1 : ∀ (h : 1 < p ∧ n ≠ 0), (go n p h).snd * p ^ (go n p h).fst = n
⊢ (p.maxPowDvdDiv n).snd * p ^ (p.maxPowDvdDiv n).fst = n
have case2 : ∀ (h : ¬(1 < p ∧ n ≠ 0)), Prod.snd (α := ℕ) (0, n) * HPow.hPow (β := ℕ) p (Prod.fst (0, n)) = n
Tactic: fun_cases maxPowDvdDiv with
  | case1 h => exact go_spec h |>.1
  | case2 h => simp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
⊢ p ^ padicValNat p n * n.divMaxPow p = n
have rw : n.divMaxPow p * p ^ padicValNat p n = n
Tactic: rw [Nat.mul_comm, divMaxPow_mul_pow_padicValNat]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
rw : n.divMaxPow p * p ^ padicValNat p n = n
⊢ p ^ padicValNat p n * n.divMaxPow p = n
have rw₁ : n = n
Tactic: rw [Nat.mul_comm, divMaxPow_mul_pow_padicValNat]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p k n a b : ℕ
hp : 1 < p
hn : n ≠ 0
hab : p ^ a * b = n
hb : ¬p ∣ b
⊢ p ^ k ∣ n ↔ k ≤ a
have subst : ∀ (hn : p ^ a * b ≠ 0), p ^ k ∣ p ^ a * b ↔ k ≤ a
Tactic: subst hab
Cleared hypotheses: n, hn, hab
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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
have inl : ∀ (hdvd : p ^ k ∣ p ^ a * b), False
Tactic: refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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
⊢ False
have inl : ∀ (l : ℕ) (hlt : a < a + l + 1) (hdvd : p ^ (a + l + 1) ∣ p ^ a * b), False
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt hlt
Cleared hypotheses: k, hlt, hdvd
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
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
⊢ False
have hdvd₁ : 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
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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
have inr : p ^ k ∣ p ^ a
Tactic: refine iff_of_true (Nat.dvd_mul_right_of_dvd ?_ _) hle
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
⊢ p ^ k ∣ p ^ a * b ↔ k ≤ a
have x : 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
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n
have inl : ∀ (hp : Ne (α := ℕ) 0 1), HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
Tactic: obtain rfl | hp₁ : p = 0 ∨ 1 < p := by grind
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
inl : ∀ (hp : Ne (α := ℕ) 0 1), HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n
have inr : ∀ (hp₁ : 1 < p), p ^ k ∣ n ↔ k ≤ padicValNat p n
Tactic: obtain rfl | hp₁ : p = 0 ∨ 1 < p := by grind
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
k n : ℕ
hn : n ≠ 0
hp : Ne (α := ℕ) 0 1
⊢ HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
have inl : HPow.hPow (α := ℕ) (β := ℕ) 0 0 ∣ n ↔ 0 ≤ padicValNat 0 n
Tactic: rcases k.eq_zero_or_pos with rfl | hk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
k n : ℕ
hn : n ≠ 0
hp : Ne (α := ℕ) 0 1
inl : HPow.hPow (α := ℕ) (β := ℕ) 0 0 ∣ n ↔ 0 ≤ padicValNat 0 n
⊢ HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
have inl₁ : ∀ (hk : k > 0), HPow.hPow (α := ℕ) 0 k ∣ n ↔ k ≤ padicValNat 0 n
Tactic: rcases k.eq_zero_or_pos with rfl | hk
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
⊢ p.maxPowDvdDiv n = (k, l)
have inl : ∀ (h : HPow.hPow (α := ℕ) 0 k * l = n) (hl : ¬0 ∣ l), maxPowDvdDiv 0 n = (k, l)
Tactic: obtain rfl | rfl | hp : p = 0 ∨ p = 1 ∨ 1 < p := by grind
Cleared hypotheses: p, h, hl
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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)
⊢ p.maxPowDvdDiv n = (k, l)
have inr : ∀ (h : HPow.hPow (α := ℕ) 1 k * l = n) (hl : ¬1 ∣ l), maxPowDvdDiv 1 n = (k, l)
Tactic: obtain rfl | rfl | hp : p = 0 ∨ p = 1 ∨ 1 < p := by grind
Cleared hypotheses: p, h, hl
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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)
⊢ p.maxPowDvdDiv n = (k, l)
have inr₁ : ∀ (hp : 1 < p), p.maxPowDvdDiv n = (k, l)
Tactic: obtain rfl | rfl | hp : p = 0 ∨ p = 1 ∨ 1 < p := by grind
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
n k l : ℕ
hn : n ≠ 0
h : HPow.hPow (α := ℕ) 0 k * l = n
hl : ¬0 ∣ l
⊢ maxPowDvdDiv 0 n = (k, l)
have inl : k = 0 → maxPowDvdDiv 0 n = (k, l)
Tactic: cases k.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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)
⊢ maxPowDvdDiv 0 n = (k, l)
have inl₁ : k > 0 → maxPowDvdDiv 0 n = (k, l)
Tactic: cases k.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k = (p.maxPowDvdDiv n).fst
have h₁ : k ≤ (p.maxPowDvdDiv n).fst
Tactic: apply Nat.le_antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
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
⊢ k = (p.maxPowDvdDiv n).fst
have h₂ : (p.maxPowDvdDiv n).fst ≤ k
Tactic: apply Nat.le_antisymm
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ (p.maxPowDvdDiv n).fst
have h₁ : k ≤ k
Tactic: rw [← padicValNat, ← pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn,
            pow_dvd_iff_le_of_spec hp hn h hl]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ k
have h₂ : (p.maxPowDvdDiv n).fst ≤ padicValNat p n
Tactic: rw [← pow_dvd_iff_le_of_spec hp hn h hl, pow_dvd_iff_le_padicValNat (Nat.ne_of_gt hp) hn]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (hypothesis)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)
have hk : 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
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)
have inr : ∀ (h : l = n.divMaxPow p) (hl : ¬p ∣ l) (hp : 1 < p) (hk : k = (p.maxPowDvdDiv n).fst), p.maxPowDvdDiv n = (k, l)
Tactic: rw [← pow_padicValNat_mul_divMaxPow p n, hk, padicValNat, Nat.mul_left_cancel_iff] at h
Cleared hypotheses: h, hl, hp, hk
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
inr : ∀ (h : l = n.divMaxPow p) (hl : ¬p ∣ l) (hp : 1 < p) (hk : k = (p.maxPowDvdDiv n).fst), p.maxPowDvdDiv n = (k, l)
⊢ p.maxPowDvdDiv n = (k, l)
have inr₁ : ∀ (h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p) (hl : ¬p ∣ l) (hp : 1 < p)
  (hk : k = (p.maxPowDvdDiv n).fst), 0 < p ^ (p.maxPowDvdDiv n).fst
Tactic: rw [← pow_padicValNat_mul_divMaxPow p n, hk, padicValNat, Nat.mul_left_cancel_iff] at h
Cleared hypotheses: h, hl, hp, hk
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)
have hn₁ : p ^ k * n ≠ 0
Tactic: apply maxPowDvdDiv_of_pow_mul_eq
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
hn₁ : p ^ k * n ≠ 0
⊢ p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)
have h : p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
Tactic: apply maxPowDvdDiv_of_pow_mul_eq
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
hn₁ : p ^ k * n ≠ 0
h : p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
⊢ p.maxPowDvdDiv (p ^ k * n) = (padicValNat p n + k, n.divMaxPow p)
have hl : ¬p ∣ n.divMaxPow p
Tactic: apply maxPowDvdDiv_of_pow_mul_eq
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
have h : p ^ padicValNat p n * p ^ k * n.divMaxPow p = p ^ k * n
Tactic: rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
h : p ^ padicValNat p n * p ^ k * n.divMaxPow p = p ^ k * n
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
have h₁ : p ^ padicValNat p n * (p ^ k * n.divMaxPow p) = p ^ k * n
Tactic: rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
h : p ^ padicValNat p n * p ^ k * n.divMaxPow p = p ^ k * n
h₁ : p ^ padicValNat p n * (p ^ k * n.divMaxPow p) = p ^ k * n
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
have h₂ : p ^ k * (p ^ padicValNat p n * n.divMaxPow p) = p ^ k * n
Tactic: rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
h : p ^ padicValNat p n * p ^ k * n.divMaxPow p = p ^ k * n
h₁ : p ^ padicValNat p n * (p ^ k * n.divMaxPow p) = p ^ k * n
h₂ : p ^ k * (p ^ padicValNat p n * n.divMaxPow p) = p ^ k * n
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n
have h₃ : p ^ k * n = p ^ k * n
Tactic: rw [Nat.pow_add, Nat.mul_assoc, Nat.mul_left_comm, pow_padicValNat_mul_divMaxPow]
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
have inl : ∀ (hp : Ne (α := ℕ) 1 0), (HPow.hPow (α := ℕ) 1 k * n).divMaxPow 1 = n.divMaxPow 1
Tactic: obtain rfl | hp1 : p = 1 ∨ 1 < p := by grind
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
inl : ∀ (hp : Ne (α := ℕ) 1 0), (HPow.hPow (α := ℕ) 1 k * n).divMaxPow 1 = n.divMaxPow 1
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
have inr : ∀ (hp1 : 1 < p), (p ^ k * n).divMaxPow p = n.divMaxPow p
Tactic: obtain rfl | hp1 : p = 1 ∨ 1 < p := by grind
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
have inr : (p ^ k * 0).divMaxPow p = divMaxPow 0 p
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.MaxPowDiv (goal)
Goal:
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
inr : (p ^ k * 0).divMaxPow p = divMaxPow 0 p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
have inr₁ : ∀ (hn : n ≠ 0), (p ^ k * n).divMaxPow p = n.divMaxPow p
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
⊢ a ≡ b [PMOD n] ↔ a ≡ b [MOD n]
have mp : a ≡ b [PMOD n] → a ≡ b [MOD n]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
mp : a ≡ b [PMOD n] → a ≡ b [MOD n]
⊢ a ≡ b [PMOD n] ↔ a ≡ b [MOD n]
have mpr : a ≡ b [MOD n] → a ≡ b [PMOD n]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
⊢ a ≡ b [PMOD n] → a ≡ b [MOD n]
have mp : (∃ (m : ℕ), ∃ (n_1 : ℕ), m • n + a = n_1 • n + b) → a % n = b % n
Tactic: rw [modEq_iff_nsmul, Nat.ModEq]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
h : a % n = b % n
⊢ a ≡ b [PMOD n]
have mpr : (a / n) • n + b % n ≡ (b / n) • n + b % n [PMOD n]
Tactic: rw [← Nat.div_add_mod' a n, ← Nat.div_add_mod' b n, ← Nat.nsmul_eq_mul, ← Nat.nsmul_eq_mul, h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoidWithOne M
a b n : ℕ
h : a ≡ b [MOD n]
⊢ ModEq.{u_1} (M := M) (↑n : M) (↑a : M) (↑b : M)
have h₁ : a ≡ b [PMOD n]
Tactic: rw [← modEq_iff_natModEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a : ℕ
⊢ a ≡ 0 [MOD n] ↔ n ∣ a
have rw : a % n = 0 % n ↔ n ∣ a
Tactic: rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a : ℕ
rw : a % n = 0 % n ↔ n ∣ a
⊢ a ≡ 0 [MOD n] ↔ n ∣ a
have rw₁ : a % n = 0 ↔ n ∣ a
Tactic: rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a : ℕ
rw : a % n = 0 % n ↔ n ∣ a
rw₁ : a % n = 0 ↔ n ∣ a
⊢ a ≡ 0 [MOD n] ↔ n ∣ a
have rw₂ : a % n = 0 ↔ a % n = 0
Tactic: rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw₂ : Eq (α := ℤ) (↑(b % n) : ℤ) (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₂ : Eq (α := ℤ) (↑(b % n) : ℤ) (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw₃ : HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₂ : Eq (α := ℤ) (↑(b % n) : ℤ) (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₃ : HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw₄ : HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔
  (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₂ : Eq (α := ℤ) (↑(b % n) : ℤ) (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₃ : HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₄ :
  HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔
    (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw₅ : HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0 ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
rw : a % n = b % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₁ : b % n = a % n ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₂ : Eq (α := ℤ) (↑(b % n) : ℤ) (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₃ : HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = (↑(a % n) : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₄ :
  HMod.hMod (α := ℤ) (↑b : ℤ) (↑n : ℤ) = HMod.hMod (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔
    (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
rw₅ : HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0 ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n] ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
have rw₆ : HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0 ↔ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) % (↑n : ℤ) = 0
Tactic: rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ n ∣ b - a
have rw : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ n ∣ b - a
Tactic: rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : a ≤ b
rw : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ n ∣ b - a
⊢ a ≡ b [MOD n] ↔ n ∣ b - a
have rw₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(b - a) : ℤ)
Tactic: rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : a ≤ b
rw : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ n ∣ b - a
rw₁ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ Dvd.dvd (α := ℤ) (↑n : ℤ) (↑(b - a) : ℤ)
⊢ a ≡ b [MOD n] ↔ n ∣ b - a
have rw₂ : (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) ↔ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)
have rw : c * (a % n) = c * b % (c * n)
Tactic: rw [mul_mod_mul_left, mul_mod_mul_left, h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
h : a % n = b % n
rw : c * (a % n) = c * b % (c * n)
⊢ c * a % (c * n) = c * b % (c * n)
have rw₁ : c * (a % n) = c * (b % n)
Tactic: rw [mul_mod_mul_left, mul_mod_mul_left, h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
h : a % n = b % n
rw : c * (a % n) = c * b % (c * n)
rw₁ : c * (a % n) = c * (b % n)
⊢ c * a % (c * n) = c * b % (c * n)
have rw₂ : c * (b % n) = c * (b % n)
Tactic: rw [mul_mod_mul_left, mul_mod_mul_left, h]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n * c]
have rw : c * a ≡ c * b [MOD c * n]
Tactic: rw [mul_comm a, mul_comm b, mul_comm n]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ a * c ≡ b * c [MOD n]
have rw : c * a ≡ c * b [MOD n]
Tactic: rw [mul_comm a, mul_comm b]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ (d + 1) ≡ b ^ (d + 1) [MOD n]
have succ : a ^ d * a ≡ b ^ d * b [MOD n]
Tactic: rw [Nat.pow_succ, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
n a b m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]
have zero : HPow.hPow (β := ℕ) a 0 ≡ HPow.hPow (β := ℕ) b 0 [MOD n]
Tactic: induction m with
  | zero => rfl
  | succ d hd =>
    rw [Nat.pow_succ, Nat.pow_succ]
    exact hd.mul h
Cleared hypotheses: m