awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ (a + b) / c = a / c + b / c
have rw : (a / c + b / c + if c ≤ a % c + b % c then 1 else 0) = a / c + b / c
Tactic: rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_gt hc), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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
⊢ (a + b) / c = a / c + b / c
have rw₁ : a / c + b / c + 0 = a / c + b / c
Tactic: rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_gt hc), add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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
⊢ (a + b) / c = a / c + b / c
have rw₂ : a / c + 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]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c
have rw : b % c < c
Tactic: rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hca : c ∣ b
⊢ (a + b) / c = a / c + b / c
have rwa : (b + a) / c = a / c + b / c
Tactic: rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hca : c ∣ b
rwa : (b + a) / c = a / c + b / c
⊢ (a + b) / c = a / c + b / c
have rwa₁ : b / c + a / c = a / c + b / c
Tactic: rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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
⊢ (a + b) / c = a / c + b / c
have rwa₃ : a / c + b / c = a / c + b / c
Tactic: rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + 1
have rw : (a / c + b / c + if c ≤ a % c + b % c then 1 else 0) = a / c + b / c + 1
Tactic: rw [Nat.add_div hc0, if_pos hc]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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
⊢ (a + b) / c = a / c + b / c + 1
have rw₁ : a / c + b / c + 1 = a / c + b / c + 1
Tactic: rw [Nat.add_div hc0, if_pos hc]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ (a + b) / c
have rw : a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0
Tactic: rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (hypothesis)
Goal:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ False
have this : (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)
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
h : b ≤ a % n
⊢ a % n - b = (a - b) % n
have inl : ∀ (h : b ≤ a % 0), a % 0 - b = (a - b) % 0
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
h : b ≤ a % n
inl : ∀ (h : b ≤ a % 0), a % 0 - b = (a - b) % 0
⊢ a % n - b = (a - b) % n
have inr : ∀ (hn : n > 0), a % n - b = (a - b) % n
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a - b) % n
have inr : a % n - b = (n * (a / n) + a % n - b) % n
Tactic: nth_rw 2 [← div_add_mod a n]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + a % n - b) % n
have inr : a % n - b = (a % n - b) % n
Tactic: rw [Nat.add_sub_assoc h, mul_add_mod]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
Goal:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw : 2 * (m * n / 2) = 2 * (m * (n / 2)) + 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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₁ : 2 * (m * n / 2) = 2 * (m * (n / 2)) + (m - 1)
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₂ : 2 * (m * n / 2) = m * (2 * (n / 2)) + (m - 1)
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₃ : 2 * (m * n / 2) = m * (n - 1) + (m - 1)
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₄ : m * n - 1 = m * (n - 1) + (m - 1)
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₅ : m * n - 1 = m * n - m * 1 + (m - 1)
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₆ : m * n - 1 = m * n - m + (m - 1)
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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)
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₇ : m * n - 1 = m * n - m + m - 1
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.ModEq (goal)
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
⊢ 2 * (m * n / 2) = 2 * (m * (n / 2) + m / 2)
have rw₈ : m * n - 1 = m * n - 1
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)]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
m n b : ℕ
hm : m ≠ 1
hn : 0 < n
hb : log m n < b
fin : FiniteMultiplicity m n
i : ℕ
⊢ i ∈ Ico 1 (multiplicity m n + 1) ↔ i ∈ {i ∈ Ico 1 b | m ^ i ∣ n}
have simp : 1 ≤ i → i ≤ multiplicity m n → i < b
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
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
⊢ i < b
have h₁ : m ^ i ∣ n
Tactic: rw [← fin.pow_dvd_iff_le_multiplicity] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
⊢ i < b
have zero : ∀ (hm : Ne (α := ℕ) 0 1) (hb : log 0 n < b) (fin : FiniteMultiplicity 0 n) (h : HPow.hPow (α := ℕ) 0 i ∣ n), i < b
Tactic: rcases m with - | m
Cleared hypotheses: m, hm, hb, fin, h
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
⊢ i < b
have succ : ∀ (m : ℕ) (hm : m + 1 ≠ 1) (hb : log (m + 1) n < b) (fin : FiniteMultiplicity (m + 1) n) (h : (m + 1) ^ i ∣ n), i < b
Tactic: rcases m with - | m
Cleared hypotheses: m, hm, hb, fin, h
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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 < b
have zero : ∀ (h : n = 0), i < b
Tactic: rw [zero_pow, zero_dvd_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
⊢ i < b
have zero₁ : i ≠ 0
Tactic: rw [zero_pow, zero_dvd_iff] at h
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
have succ : i ≤ log (m + 1) n
Tactic: refine LE.le.trans_lt ?_ hb
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)
have rw : emultiplicity p ((n + 1) * n !) = emultiplicity p n ! + emultiplicity p (n + 1)
Tactic: rw [factorial_succ, hp.emultiplicity_mul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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)
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)
have rw₁ : emultiplicity p (n + 1) + emultiplicity p n ! = emultiplicity p n ! + emultiplicity p (n + 1)
Tactic: rw [factorial_succ, hp.emultiplicity_mul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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)
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)
have rw₂ : emultiplicity p n ! + emultiplicity p (n + 1) = emultiplicity p n ! + emultiplicity p (n + 1)
Tactic: rw [factorial_succ, hp.emultiplicity_mul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p n ! + emultiplicity p (n + 1) =
    HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞)
have 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})) : ℕ∞)
Tactic: rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
          emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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})) : ℕ∞)
⊢ emultiplicity p n ! + emultiplicity p (n + 1) =
    HAdd.hAdd (α := ℕ∞) (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) (↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) : ℕ∞)
have rw₁ : (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) + emultiplicity p (n + 1) =
  (↑(∑ i ∈ Ico 1 b, n / p ^ i) : ℕ∞) + emultiplicity p n.succ
Tactic: rw [emultiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
          emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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})) : ℕ∞) =
    (↑(∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0)) : ℕ∞)
have 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})) : ℕ)) : ℕ∞)
Tactic: rw [sum_add_distrib, sum_boole]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
n p : ℕ
hp : Prime p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have hp' : _root_.Prime p
Tactic: have hp' := hp.prime
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have h0 : 2 ≤ p
Tactic: have h0 : 2 ≤ p := hp.two_le
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have h1 : 1 ≤ p * n + 1
Tactic: have h1 : 1 ≤ p * n + 1 := Nat.le_add_left _ _
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ p * n + 1 ≤ p * (n + 1)
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
⊢ p * n + 1 ≤ p * (n + 1)
have linarith₁ : p * (n + 1) < p * n + 1 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
Goal:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have h2 : p * n + 1 ≤ p * (n + 1)
Tactic: have h2 : p * n + 1 ≤ p * (n + 1) := by linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
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)
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have h3 : p * n + 1 ≤ p * (n + 1) + 1
Tactic: have h3 : p * n + 1 ≤ p * (n + 1) + 1 := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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)! ≠ ⊤
have rw : p ≠ 1 ∧ 0 < (p * n)!
Tactic: rw [Ne, emultiplicity_eq_top, Classical.not_not, Nat.finiteMultiplicity_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
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 + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have hm : 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 _⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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)! ≠ ⊤
⊢ emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have revert : ∀ (hm : emultiplicity p (p * n)! ≠ ⊤),
  emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
Tactic: revert hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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))
⊢ emultiplicity p m = 0
have rw : ∃ (k : ℕ), p * k < m ∧ m < p * (k + 1)
Tactic: rw [emultiplicity_eq_zero, not_dvd_iff_lt_mul_succ _ hp.pos]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
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))
⊢ ∃ (k : ℕ), p * k < m ∧ m < p * (k + 1)
have hm₁ : p * n + 1 ≤ m ∧ m < p * (n + 1)
Tactic: rw [mem_Ico] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (hypothesis)
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)! ≠ ⊤),
    emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have h4 : ∀ 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⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ ∀ (hm : emultiplicity p (p * n)! ≠ ⊤),
    emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1
have simp_rw : ∀ (hm : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤),
  HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
Tactic: simp_rw [← prod_Ico_id_eq_factorial, Finset.emultiplicity_prod hp', ← sum_Ico_consecutive _ h1 h3,
    add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₁ : ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]
-- Lean 4 proof step from Mathlib.Data.Nat.Multiplicity (goal)
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
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
h : Ne (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x) ⊤
rw : ∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x = emultiplicity p (n + 1) + 1
rw₁ :
  ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + emultiplicity p (p * (n + 1)) = emultiplicity p (n + 1) + 1
⊢ HAdd.hAdd (α := ℕ∞) (∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x)
      (∑ x ∈ Ico (p * n + 1) (p * (n + 1) + 1), emultiplicity p x) =
    ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x + (emultiplicity p (n + 1) + 1)
have rw₂ : ∑ k ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p k + (emultiplicity p p + emultiplicity p (n + 1)) =
  emultiplicity p (n + 1) + 1
Tactic: rw [WithTop.add_left_inj h, sum_Ico_succ_top h2, hp.emultiplicity_mul, hp.emultiplicity_self,
    sum_congr rfl h4, sum_const_zero, zero_add, add_comm 1]