awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
succ₄ : (↑n ! : A) * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)
succ₅ : a ^ n * hI.dpow 1 a = a ^ (n + 1)
succ₆ : a ^ n * a = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₇ : a ^ n * a = a ^ n * a
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
succ₄ : (↑n ! : A) * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)
succ₅ : a ^ n * hI.dpow 1 a = a ^ (n + 1)
succ₆ : a ^ n * a = a ^ (n + 1)
succ₇ : a ^ n * a = a ^ n * a
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₈ : a * a ^ n = a * a ^ n
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ (↑n ! : A) * hI.dpow n a = a ^ n
have zero : (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
Tactic: induction n with
  | zero => rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
  | succ n ih =>
    rw [factorial_succ, mul_comm (n + 1)]
    nth_rewrite 1 [← (n + 1).choose_one_right]
    rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
zero : (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
⊢ (↑n ! : A) * hI.dpow n a = a ^ n
have succ : ∀ (n : ℕ) (ih : (↑n ! : A) * hI.dpow n a = a ^ n), (↑(n + 1)! : A) * hI.dpow (n + 1) a = a ^ (n + 1)
Tactic: induction n with
  | zero => rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
  | succ n ih =>
    rw [factorial_succ, mul_comm (n + 1)]
    nth_rewrite 1 [← (n + 1).choose_one_right]
    rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
have rw : hI.dpow n (HMul.hMul (α := A) 0 0) = HMul.hMul (α := A) 0 0
Tactic: rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
    zero_pow hn, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
rw : hI.dpow n (HMul.hMul (α := A) 0 0) = HMul.hMul (α := A) 0 0
⊢ hI.dpow n 0 = 0
have rw₁ : HPow.hPow (α := A) 0 n * hI.dpow n 0 = HMul.hMul (α := A) 0 0
Tactic: rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
    zero_pow hn, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
rw : hI.dpow n (HMul.hMul (α := A) 0 0) = HMul.hMul (α := A) 0 0
rw₁ : HPow.hPow (α := A) 0 n * hI.dpow n 0 = HMul.hMul (α := A) 0 0
⊢ hI.dpow n 0 = 0
have rw₂ : 0 * hI.dpow n 0 = HMul.hMul (α := A) 0 0
Tactic: rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
    zero_pow hn, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
rw : hI.dpow n (HMul.hMul (α := A) 0 0) = HMul.hMul (α := A) 0 0
rw₁ : HPow.hPow (α := A) 0 n * hI.dpow n 0 = HMul.hMul (α := A) 0 0
rw₂ : 0 * hI.dpow n 0 = HMul.hMul (α := A) 0 0
⊢ hI.dpow n 0 = 0
have rw₃ : 0 = HMul.hMul (α := A) 0 0
Tactic: rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
    zero_pow hn, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
rw : hI.dpow n (HMul.hMul (α := A) 0 0) = HMul.hMul (α := A) 0 0
rw₁ : HPow.hPow (α := A) 0 n * hI.dpow n 0 = HMul.hMul (α := A) 0 0
rw₂ : 0 * hI.dpow n 0 = HMul.hMul (α := A) 0 0
rw₃ : 0 = HMul.hMul (α := A) 0 0
⊢ hI.dpow n 0 = 0
have rw₄ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
    zero_pow hn, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
have rw : (↑n ! : A) * hI.dpow n a = HMul.hMul (α := A) (↑n : A) (↑(n - 1)! : A) * hI.dpow n a
Tactic: rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
rw : (↑n ! : A) * hI.dpow n a = HMul.hMul (α := A) (↑n : A) (↑(n - 1)! : A) * hI.dpow n a
⊢ (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
have rw₁ : (↑n ! : A) * hI.dpow n a = (↑(n * (n - 1)!) : A) * hI.dpow n a
Tactic: rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
rw : (↑n ! : A) * hI.dpow n a = HMul.hMul (α := A) (↑n : A) (↑(n - 1)! : A) * hI.dpow n a
rw₁ : (↑n ! : A) * hI.dpow n a = (↑(n * (n - 1)!) : A) * hI.dpow n a
⊢ (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
have rw₂ : (↑n ! : A) * hI.dpow n a = (↑n ! : A) * hI.dpow n a
Tactic: rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
⊢ a ^ n = 0
have h_fac : (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
Tactic: have h_fac : (n ! : A) * hI.dpow n a = n • ((n - 1)! : A) * hI.dpow n a := by
    rw [nsmul_eq_mul, ← cast_mul, mul_factorial_pred hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
hI : DividedPowers I
ha : a ∈ I
h_fac : (↑n ! : A) * hI.dpow n a = HSMul.hSMul (β := A) n (↑(n - 1)! : A) * hI.dpow n a
⊢ a ^ n = 0
have rw : n • ((↑(n - 1)! : A) * hI.dpow n a) = 0
Tactic: rw [← hI.factorial_mul_dpow_eq_pow ha, h_fac, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a_1 : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ hI.dpow n (a • b) = hJ.dpow n (a • b)
have smul : (↑n ! : A) * hJ.dpow n b * hI.dpow n a = (↑n ! : A) * hI.dpow n a * hJ.dpow n b
Tactic: rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ hI.dpow n (x + y) = hJ.dpow n (x + y)
have add : Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 x * hI.dpow k.2 y)
  (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hJ.dpow k.1 x * hJ.dpow k.2 y)
Tactic: rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy),
      hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
⊢ Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 x * hI.dpow k.2 y)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hJ.dpow k.1 x * hJ.dpow k.2 y)
have add : ∀ x_1 ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow x_1.1 x * hI.dpow x_1.2 y = hJ.dpow x_1.1 x * hJ.dpow x_1.2 y
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
h : k ∈ @antidiagonal _ instAddMonoid _ n
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
have add : hJ.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
Tactic: rw [hx', hy']
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x
hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y
n : ℕ
k : ℕ × ℕ
h : k ∈ @antidiagonal _ instAddMonoid _ n
add : hJ.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
⊢ hI.dpow k.1 x * hI.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
have add₁ : hJ.dpow k.1 x * hJ.dpow k.2 y = hJ.dpow k.1 x * hJ.dpow k.2 y
Tactic: rw [hx', hy']
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
ha : a ∈ I • J
⊢ hI.dpow n a = hJ.dpow n a
have smul : ∀ (a : A) (ha : a ∈ I) (b : A) (hb : b ∈ J) {n : ℕ}, hI.dpow n (a • b) = hJ.dpow n (a • b)
Tactic: induction ha using Submodule.smul_induction_on' generalizing n with
  | smul a ha b hb =>
    rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]
    ring
  | add x hx y hy hx' hy' =>
    rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy),
      hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]
    apply sum_congr rfl
    intro k _
    rw [hx', hy']
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
n : ℕ
ha : a ∈ I • J
smul : ∀ (a : A) (ha : a ∈ I) (b : A) (hb : b ∈ J) {n : ℕ}, hI.dpow n (a • b) = hJ.dpow n (a • b)
⊢ hI.dpow n a = hJ.dpow n a
have add : ∀ (x : A) (hx : x ∈ I • J) (y : A) (hy : y ∈ I • J) (hx' : ∀ {n : ℕ}, hI.dpow n x = hJ.dpow n x)
  (hy' : ∀ {n : ℕ}, hI.dpow n y = hJ.dpow n y) {n : ℕ}, hI.dpow n (x + y) = hJ.dpow n (x + y)
Tactic: induction ha using Submodule.smul_induction_on' generalizing n with
  | smul a ha b hb =>
    rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]
    ring
  | add x hx y hy hx' hy' =>
    rw [hI.dpow_add (mul_le_right hx) (mul_le_right hy),
      hJ.dpow_add (mul_le_left hx) (mul_le_left hy)]
    apply sum_congr rfl
    intro k _
    rw [hx', hy']
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
have empty : 1 = hI.dpow 0 a
Tactic: simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
⊢ 1 = hI.dpow 0 a
have empty : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [hI.dpow_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
⊢ ∏ i ∈ insert a_1 s, hI.dpow (n i) a = (↑(multinomial (insert a_1 s) n) : A) * hI.dpow ((insert a_1 s).sum n) a
have insert : HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) *
    hI.dpow (∑ x ∈ insert a_1 s, n x) a =
  (↑(multinomial (insert a_1 s) n) : A) * hI.dpow ((insert a_1 s).sum n) a
Tactic: rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) *
      hI.dpow (∑ x ∈ insert a_1 s, n x) a =
    (↑(multinomial (insert a_1 s) n) : A) * hI.dpow ((insert a_1 s).sum n) a
have apply : HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
  (↑(multinomial (insert a_1 s) n) : A)
Tactic: apply congr_arg₂ _ _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑(multinomial (insert a_1 s) n) : A)
have rw : HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
  (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
rw :
  HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑(multinomial (insert a_1 s) n) : A)
have rw₁ : HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
  (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
rw :
  HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
rw₁ :
  HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑(multinomial (insert a_1 s) n) : A)
have rw₂ : HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
  HMul.hMul (α := A) (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1)) : A) (↑(multinomial s n) : A)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a_1 : ι
s : Finset ι
hi : a_1 ∉ s
hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
rw :
  HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
rw₁ :
  HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
    (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1) * multinomial s n) : A)
rw₂ :
  HMul.hMul (α := A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) (↑(multinomial s n) : A) =
    HMul.hMul (α := A) (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1)) : A) (↑(multinomial s n) : A)
⊢ HMul.hMul (α := A) (↑(multinomial s n) : A) (↑(Nat.choose (∑ x ∈ insert a_1 s, n x) (n a_1)) : A) =
    (↑(multinomial (insert a_1 s) n) : A)
have rw₃ : HMul.hMul (α := A) (↑((n a_1 + ∑ x ∈ s, n x).choose (n a_1)) : A) (↑(multinomial s n) : A) =
  HMul.hMul (α := A) (↑((n a_1 + ∑ i ∈ s, n i).choose (n a_1)) : A) (↑(multinomial s n) : A)
Tactic: rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
have empty : ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
empty : ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
⊢ ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
have insert : ∀ (a_1 : ι) (s : Finset ι) (hi : a_1 ∉ s)
  (hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a),
  ∏ i ∈ insert a_1 s, hI.dpow (n i) a = (↑(multinomial (insert a_1 s) n) : A) * hI.dpow ((insert a_1 s).sum n) a
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
have empty : ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
s : Finset ι
n : ι → ℕ
ha : a ∈ I
empty : ∏ i ∈ ∅, hI.dpow (n i) a = (↑(multinomial ∅ n) : A) * hI.dpow (Finset.sum ∅ n) a
⊢ ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a
have insert : ∀ (a_1 : ι) (s : Finset ι) (hi : a_1 ∉ s)
  (hrec : ∏ i ∈ s, hI.dpow (n i) a = (↑(multinomial s n) : A) * hI.dpow (s.sum n) a),
  ∏ i ∈ insert a_1 s, hI.dpow (n i) a = (↑(multinomial (insert a_1 s) n) : A) * hI.dpow ((insert a_1 s).sum n) a
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]
    rw [hI.dpow_zero ha]
  | insert _ _ hi hrec =>
    rw [prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
      mul_assoc, hI.mul_dpow ha, ← sum_insert hi, ← mul_assoc]
    apply congr_arg₂ _ _ rfl
    rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_add :
  ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, dpow k.1 x * dpow k.2 y
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
s : Finset ι
x : ι → M
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
⊢ dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
have dpow_add₁ : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
Tactic: simp only [sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add
Cleared hypotheses: dpow_add
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
⊢ dpow n (Finset.sum ∅ x) = ∑ k ∈ Finset.sym ∅ n, ∏ i ∈ ∅, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
have empty : dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)
Tactic: simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]