awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ (a % c + b % c) / c < 2

Tactic:
have h2 : (a % c + b % c) / c < 2 :=
        Nat.div_lt_of_lt_mul
          (by
            rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
⊢ 0 < (a % c + b % c) / c

Tactic:
have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
pos : (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₁ : c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₂ : c + ((a % c + b % c) % c + c * ((a % c + b % c) / c)) = a % c + b % c + c * ((a % c + b % c) / c)
pos₃ : c + (a % c + b % c) = a % c + b % c + c * ((a % c + b % c) / c)
pos₄ : c + (a % c + b % c) = a % c + b % c + c * 1
pos₅ : c + (a % c + b % c) = a % c + b % c + c
pos₆ pos₇ : a % c + b % c + c = a % c + b % c + c
⊢ (a % c + b % c) % c + c = a % c + b % c

Tactic:
rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]

Premises used: add_assoc, add_comm, Nat.mod_add_div, le_antisymm, Nat.le_of_lt_succ, add_right_cancel_iff, mul_one
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : ¬c ≤ a % c + b % c
neg : a % c + b % c + 0 = a % c + b % c
neg₁ neg₂ : a % c + b % c = a % c + b % c
⊢ (a % c + b % c) % c + 0 = a % c + b % c

Tactic:
rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]

Premises used: lt_of_not_ge, Nat.mod_eq_of_lt, add_zero
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc : a % c + b % c < c
rw : (a + b) % c = (a + b) % c + if c ≤ a % c + b % c then c else 0
rw₁ : (a + b) % c = (a + b) % c + 0
rw₂ rw₃ : (a + b) % c = (a + b) % c
⊢ (a + b) % c = a % c + b % c

Tactic:
rw [← add_mod_add_ite, if_neg (not_le_of_gt hc), add_zero]

Premises used: Nat.add_mod_add_ite, not_le_of_gt, add_zero, if_neg
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc : c ≤ a % c + b % c
rw : (a + b) % c + c = (a + b) % c + if c ≤ a % c + b % c then c else 0
rw₁ rw₂ : (a + b) % c + c = (a + b) % c + c
⊢ (a + b) % c + c = a % c + b % c

Tactic:
rw [← add_mod_add_ite, if_pos hc]

Premises used: if_pos, Nat.add_mod_add_ite
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc : a % c + b % c < c
hc0 : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
simp [hc0]
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
rw : (a / c + b / c + if c ≤ a % c + b % c then 1 else 0) = a / c + b / c
rw₁ : a / c + b / c + 0 = a / c + b / c
rw₂ rw₃ : a / c + b / c = a / c + b / c
⊢ (a + b) / c = a / c + b / c

Tactic:
rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_gt hc), add_zero]

Premises used: Nat.add_div, Nat.pos_of_ne_zero, not_le_of_gt, add_zero, if_neg
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hca : c ∣ a
h : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
rw : b % c < c
⊢ a % c + b % c < c

Tactic:
rw [Nat.mod_eq_zero_of_dvd hca, zero_add]

Premises used: zero_add, Nat.mod_eq_zero_of_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c

Tactic:
Nat.mod_lt _ (zero_lt_of_ne_zero h)

Premises used: Nat.zero_lt_of_ne_zero, Nat.mod_lt
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ b % c < c

Tactic:
exact Nat.mod_lt _ (zero_lt_of_ne_zero h)

Premises used: Nat.zero_lt_of_ne_zero, Nat.mod_lt
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hca : c ∣ b
rwa : (b + a) / c = a / c + b / c
rwa₁ : b / c + a / c = a / c + b / c
rwa₂ : c ∣ b
rwa₃ : a / c + b / c = a / c + b / c
rwa₄ : c ∣ b
rwa₅ : a / c + b / c = a / c + b / c
rwa₆ rwa₇ rwa₈ : c ∣ b
⊢ (a + b) / c = a / c + b / c

Tactic:
rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]

Premises used: add_comm, Nat.add_div_of_dvd_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
rw : (a / c + b / c + if c ≤ a % c + b % c then 1 else 0) = a / c + b / c + 1
rw₁ rw₂ : a / c + b / c + 1 = a / c + b / c + 1
⊢ (a + b) / c = a / c + b / c + 1

Tactic:
rw [Nat.add_div hc0, if_pos hc]

Premises used: Nat.add_div, if_pos
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc0 : c = 0
⊢ a / c + b / c ≤ (a + b) / c

Tactic:
simp [hc0]
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc0 : ¬c = 0
rw : a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0
⊢ a / c + b / c ≤ (a + b) / c

Tactic:
rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]

Premises used: Nat.add_div, Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Tactic:
Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Tactic:
exact Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ (a + b) % c = a % c + b % c

Tactic:
have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
this : (a + b) % c = a % c + b % c
⊢ False

Tactic:
simp_all [dvd_iff_mod_eq_zero]

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : b ≤ a % n
inl : ∀ (h : b ≤ a % 0), a % 0 - b = (a - b) % 0
inr : ∀ (hn : n > 0), a % n - b = (a - b) % n
⊢ a % n - b = (a - b) % n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b : ℕ
h : b ≤ a % 0
⊢ a % 0 - b = (a - b) % 0

Tactic:
simp only [mod_zero]

Premises used: Nat.mod_zero
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : b ≤ a % n
hn : n > 0
inr : a % n - b = (n * (a / n) + a % n - b) % n
⊢ a % n - b = (a - b) % n

Tactic:
nth_rw 2 [← div_add_mod a n]

Premises used: Nat.div_add_mod
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : b ≤ a % n
hn : n > 0
inr : a % n - b = (a % n - b) % n
⊢ a % n - b = (n * (a / n) + a % n - b) % n

Tactic:
rw [Nat.add_sub_assoc h, mul_add_mod]

Premises used: Nat.add_sub_assoc, Nat.mul_add_mod
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a % n - b) % n

Tactic:
(mod_eq_of_lt <| (sub_le ..).trans_lt (mod_lt a hn)).symm

Premises used: Nat.sub_le, Nat.mod_eq_of_lt, Nat.mod_lt, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a % n - b) % n

Tactic:
exact (mod_eq_of_lt <| (sub_le ..).trans_lt (mod_lt a hn)).symm

Premises used: Nat.sub_le, Nat.mod_eq_of_lt, Nat.mod_lt, Eq.symm, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n m : ℕ
⊢ n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1

Tactic:
simpa [Nat.ModEq] using @ModEq.mul 2 n 1 m 1

Premises used: Nat.ModEq.mul, Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
h : n = 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 1 ≤ m

Tactic:
lia
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
rw : 2 * (m * n / 2) = 2 * (m * (n / 2)) + 2 * (m / 2)
rw₁ : 2 * (m * n / 2) = 2 * (m * (n / 2)) + (m - 1)
rw₂ : 2 * (m * n / 2) = m * (2 * (n / 2)) + (m - 1)
rw₃ : 2 * (m * n / 2) = m * (n - 1) + (m - 1)
rw₄ : m * n - 1 = m * (n - 1) + (m - 1)
rw₅ : m * n - 1 = m * n - m * 1 + (m - 1)
rw₆ : m * n - 1 = m * n - m + (m - 1)
rw₇ : m * n - 1 = m * n - m + m - 1
rw₈ rw₉ : m * n - 1 = m * n - 1
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)

Tactic:
rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
      Nat.add_sub_assoc (by lia), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]

Premises used: Nat.le_mul_of_pos_right, Nat.add_sub_assoc, Nat.two_mul_odd_div_two, mul_left_comm, Nat.sub_add_cancel, Nat.odd_mul_odd, mul_add, mul_one, Nat.mul_sub
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n : ℕ
⊢ n % 4 = 1 → n % 2 = 1

Tactic:
simpa [ModEq] using @ModEq.of_mul_left 2 n 1 2

Premises used: Nat.ModEq.of_mul_left, Nat.ModEq, OfNat.ofNat
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n : ℕ
⊢ n % 4 = 3 → n % 2 = 1

Tactic:
simpa [ModEq] using @ModEq.of_mul_left 2 n 3 2

Premises used: Nat.ModEq.of_mul_left, Nat.ModEq, OfNat.ofNat
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n : ℕ
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3

Tactic:
decide
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ LT.lt (α := ℕ) 0 4

Tactic:
lia
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n : ℕ
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → m = 1 ∨ m = 3
hn : n % 2 = 1
⊢ Dvd.dvd (α := ℕ) 2 4

Tactic:
decide
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b n : ℕ
h : a ≡ b [MOD n]
hb : b < n
⊢ a % n = b

Tactic:
Eq.trans h (mod_eq_of_lt hb)

Premises used: Nat.mod_eq_of_lt, Eq.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h0 : a / n = b / n
h1 : a ≡ b [MOD n]
⊢ a = b

Tactic:
ext_div_mod h0 h1

Premises used: Nat.ext_div_mod
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a = b ↔ a / n = b / n ∧ a ≡ b [MOD n]

Tactic:
ext_div_mod_iff _ _ _

Premises used: Nat.ModEq, Nat.ext_div_mod_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a / n = b / n
⊢ a ≡ b [MOD n] ↔ a = b

Tactic:
grind [ext_div_modEq_iff]

Premises used: Nat.ext_div_modEq_iff
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
⊢ emultiplicity m n = (↑(#(Ico 1 (multiplicity m n + 1))) : ℕ∞)

Tactic:
simp [fin.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
simp : 1 ≤ i → i ≤ multiplicity m n → i < b
⊢ i ∈ Ico 1 (multiplicity m n + 1) ↔ i ∈ {i ∈ Ico 1 b | m ^ i ∣ n}

Tactic:
simp only [mem_Ico, Nat.lt_succ_iff,
              fin.pow_dvd_iff_le_multiplicity, mem_filter,
              and_assoc, and_congr_right_iff, iff_and_self]

Premises used: and_congr_right_iff, Nat.lt_succ_iff, and_assoc, FiniteMultiplicity.pow_dvd_iff_le_multiplicity, Finset.mem_filter, iff_and_self, Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
h : i ≤ multiplicity m n
⊢ m ^ i ∣ n

Tactic:
rw [← fin.pow_dvd_iff_le_multiplicity] at h

Premises used: FiniteMultiplicity.pow_dvd_iff_le_multiplicity
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
hi : 1 ≤ i
h : m ^ i ∣ n
zero :
  ∀ (hm : Ne (α := ℕ) 0 1) (hb : log 0 n < b) (fin : FiniteMultiplicity 0 n) (h : HPow.hPow (α := ℕ) 0 i ∣ n), i < b
succ :
  ∀ (m : ℕ) (hm : m + 1 ≠ 1) (hb : log (m + 1) n < b) (fin : FiniteMultiplicity (m + 1) n) (h : (m + 1) ^ i ∣ n), i < b
⊢ i < b

Tactic:
rcases m with - | m
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : Ne (α := ℕ) 0 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : HPow.hPow (α := ℕ) 0 i ∣ n
zero : ∀ (h : n = 0), i < b
zero₁ : i ≠ 0
⊢ i < b

Tactic:
rw [zero_pow, zero_dvd_iff] at h

Premises used: zero_dvd_iff, zero_pow
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : Ne (α := ℕ) 0 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : n = 0
⊢ i < b

Tactic:
(hn.ne' h).elim

Premises used: False.elim, LT.lt.ne'
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : Ne (α := ℕ) 0 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : HPow.hPow (α := ℕ) 0 i ∣ n
⊢ i ≠ 0

Tactic:
one_le_iff_ne_zero.1 hi

Premises used: Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : Ne (α := ℕ) 0 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : n = 0
⊢ i < b

Tactic:
exacts [(hn.ne' h).elim, one_le_iff_ne_zero.1 hi]

Premises used: False.elim, LT.lt.ne', Iff.mp, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i < b

Tactic:
LE.le.trans_lt ?_ hb

Premises used: LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
succ : i ≤ log (m + 1) n
⊢ i < b

Tactic:
refine LE.le.trans_lt ?_ hb

Premises used: LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i ≤ log (m + 1) n

Tactic:
le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
                (le_of_dvd hn h)

Premises used: Iff.mpr, Nat.le_log_of_pow_le, Nat.succ_ne_zero, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i ≤ log (m + 1) n

Tactic:
exact le_log_of_pow_le (one_lt_iff_ne_zero_and_ne_one.2 ⟨m.succ_ne_zero, hm⟩)
                (le_of_dvd hn h)

Premises used: Iff.mpr, Nat.le_log_of_pow_le, Nat.succ_ne_zero, And.intro, Nat.one_lt_iff_ne_zero_and_ne_one, Nat.le_of_dvd
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
⊢ emultiplicity p 1 = 0

Tactic:
emultiplicity_of_one_right hp.prime.not_unit

Premises used: emultiplicity_of_one_right, Nat.Prime.prime, Prime.not_unit
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p m n : ℕ
hp : Prime p
⊢ emultiplicity p (m * n) = emultiplicity p m + emultiplicity p n

Tactic:
_root_.emultiplicity_mul hp.prime

Premises used: Nat.Prime.prime, emultiplicity_mul
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p m n : ℕ
hp : Prime p
⊢ emultiplicity p (m ^ n) = (↑n : ℕ∞) * emultiplicity p m

Tactic:
_root_.emultiplicity_pow hp.prime

Premises used: Nat.Prime.prime, emultiplicity_pow
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
⊢ emultiplicity p p = 1

Tactic:
(Nat.finiteMultiplicity_iff.2 ⟨hp.ne_one, hp.pos⟩).emultiplicity_self

Premises used: Iff.mpr, FiniteMultiplicity.emultiplicity_self, Nat.Prime.pos, Nat.Prime.ne_one, And.intro, Nat.finiteMultiplicity_iff
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p n : ℕ
hp : Prime p
⊢ emultiplicity p (p ^ n) = (↑n : ℕ∞)

Tactic:
_root_.emultiplicity_pow_self hp.ne_zero hp.prime.not_unit n

Premises used: Nat.Prime.prime, emultiplicity_pow_self, Prime.not_unit, Nat.Prime.ne_zero
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
b : ℕ
h : log p 0 < b
⊢ emultiplicity p 0! = (↑(∑ i ∈ Ico 1 b, 0 / p ^ i) : ℕ∞)

Tactic:
simp [Ico, hp.emultiplicity_one]

Premises used: Finset.Ico, Nat.Prime.emultiplicity_one
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw : emultiplicity p ((n + 1) * n !) = emultiplicity p n ! + emultiplicity p (n + 1)
rw₁ : emultiplicity p (n + 1) + emultiplicity p n ! = emultiplicity p n ! + emultiplicity p (n + 1)
rw₂ rw₃ : emultiplicity p n ! + emultiplicity p (n + 1) = emultiplicity p n ! + emultiplicity p (n + 1)
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)

Tactic:
rw [factorial_succ, hp.emultiplicity_mul, add_comm]

Premises used: Nat.factorial_succ, add_comm, Nat.Prime.emultiplicity_mul
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw :
  (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) + emultiplicity p (n + 1) =
    HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞)
rw₁ rw₂ :
  (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) + emultiplicity p (n + 1) =
    (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) + emultiplicity p n.succ
⊢ emultiplicity p n ! + emultiplicity p (n + 1) =
    HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞)

Tactic:
rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
          emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]

Premises used: Nat.le_succ, Nat.Prime.ne_one, Nat.succ_pos, LE.le.trans_lt, Nat.emultiplicity_eq_card_pow_dvd, Nat.log_mono_right
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
rw :
  HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞) =
    (↑(HAdd.hAdd (α := ℕ) (∑ x ∈ Ico 1 b, n / p ^ x) (↑(#({x ∈ Ico 1 b | p ^ x ∣ n + 1})) : ℕ)) : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞) =
    (↑(∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0)) : ℕ∞)

Tactic:
rw [sum_add_distrib, sum_boole]

Premises used: Finset.sum_add_distrib, Finset.sum_boole
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞) =
    (↑(HAdd.hAdd (α := ℕ) (∑ x ∈ Ico 1 b, n / p ^ x) (↑(#({x ∈ Ico 1 b | p ^ x ∣ n + 1})) : ℕ)) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
⊢ (p - 1) * multiplicity p n ! = n - (p.digits n).sum

Tactic:
simp only [multiplicity_eq_of_emultiplicity_eq_some <|
      emultiplicity_factorial hp <| lt_succ_of_lt <| Nat.lt_add_one (log p n),
    ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
    sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]

Premises used: Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits, Nat.Prime.emultiplicity_factorial, Nat.lt_add_one, Finset.sum_Ico_add', Nat.Ico_zero_eq_range, Nat.lt_succ_of_lt, Nat.log, OfNat.ofNat, multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
⊢ _root_.Prime p

Tactic:
have hp' := hp.prime
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ 2 ≤ p

Tactic:
have h0 : 2 ≤ p := hp.two_le
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ 1 ≤ p * n + 1

Tactic:
have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
linarith :
  p * (n + 1) < p * n + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
        ((↑p : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - (HMul.hMul (α := ℤ) (↑p : ℤ) (↑n : ℤ) + 1)) =
      0
linarith₁ : p * (n + 1) < p * n + 1 → GT.gt (α := ℤ) 2 0
⊢ p * n + 1 ≤ p * (n + 1)

Tactic:
linarith
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)

Tactic:
have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
⊢ p * n + 1 ≤ p * (n + 1) + 1

Tactic:
have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
rw : p ≠ 1 ∧ 0 < (p * n)!
⊢ emultiplicity p (p * n)! ≠ ⊤

Tactic:
rw [Ne, emultiplicity_eq_top, Classical.not_not, Nat.finiteMultiplicity_iff]

Premises used: Classical.not_not, emultiplicity_eq_top, Ne, Nat.finiteMultiplicity_iff
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ p ≠ 1 ∧ 0 < (p * n)!

Tactic:
⟨hp.ne_one, factorial_pos _⟩

Premises used: Nat.Prime.ne_one, And.intro, Nat.factorial_pos
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ p ≠ 1 ∧ 0 < (p * n)!

Tactic:
exact ⟨hp.ne_one, factorial_pos _⟩
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ emultiplicity p (p * n)! ≠ ⊤

Tactic:
have hm : emultiplicity p (p * n)! ≠ ⊤ := by
    rw [Ne, emultiplicity_eq_top, Classical.not_not, Nat.finiteMultiplicity_iff]
    exact ⟨hp.ne_one, factorial_pos _⟩
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
hm : emultiplicity p (p * n)! ≠ ⊤
revert :
  ∀ (hm : emultiplicity p (p * n)! ≠ ⊤),
    emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
revert hm
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
rw : ∃ (k : ℕ), p * k < m ∧ m < p * (k + 1)
⊢ emultiplicity p m = 0

Tactic:
rw [emultiplicity_eq_zero, not_dvd_iff_lt_mul_succ _ hp.pos]

Premises used: emultiplicity_eq_zero, Nat.Prime.pos, Nat.not_dvd_iff_lt_mul_succ
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ p * n + 1 ≤ m ∧ m < p * (n + 1)

Tactic:
rw [mem_Ico] at hm

Premises used: Finset.mem_Ico
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ (k : ℕ), p * k < m ∧ m < p * (k + 1)

Tactic:
⟨n, lt_of_succ_le hm.1, hm.2⟩

Premises used: Nat.lt_of_succ_le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
m : ℕ
hm : p * n + 1 ≤ m ∧ m < p * (n + 1)
⊢ ∃ (k : ℕ), p * k < m ∧ m < p * (k + 1)

Tactic:
exact ⟨n, lt_of_succ_le hm.1, hm.2⟩
-- Module: Mathlib.Data.Nat.Multiplicity
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
⊢ ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0

Tactic:
have h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0 := by
    intro m hm
    rw [emultiplicity_eq_zero, not_dvd_iff_lt_mul_succ _ hp.pos]
    rw [mem_Ico] at hm
    exact ⟨n, lt_of_succ_le hm.1, hm.2⟩