-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem prod_dpow {ι : Type*} {s : Finset ι} {n : ι → ℕ} (ha : a ∈ I) :
    (s.prod fun i ↦ hI.dpow (n i) a) = multinomial s n * hI.dpow (s.sum n) a

Proof state:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * hI.dpow (∑ x ∈ insert a✝ s✝, n x) a =
    ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a

Tactic:
apply congr_arg₂ _ _ rfl

Result:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(multinomial (insert a✝ s✝) n)

Proof state:
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) * hI.dpow (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]

Result:
no goals

Proof state:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ∏ i ∈ insert a✝ s✝, hI.dpow (n i) a = ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ 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]

Result:
case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * hI.dpow (∑ x ∈ insert a✝ s✝, n x) a =
    ↑(multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a

Proof state:
case empty
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) * hI.dpow (∅.sum n) a

Tactic:
simp only [prod_empty, multinomial_empty, cast_one, sum_empty, one_mul]

Result:
case empty
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

Proof state:
case empty
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

Tactic:
rw [hI.dpow_zero ha]

Result:
no goals

Proof state:
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) * hI.dpow (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]

Result:
no goals

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ι : Type u_2
n : ι → ℕ
ha : a ∈ I
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(multinomial (insert a✝ s✝) n)

Tactic:
rw [multinomial_insert hi, mul_comm, cast_mul, sum_insert hi]

Result:
no goals