Theorem: DividedPowers.prod_dpow_self (DividedPowers/Basic.lean)

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
s : Finset ι
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
Tactic:
induction' s using Finset.induction with i s hi ih
State after:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = ↑(Nat.multinomial ∅ n) * hI.dpow (∅.sum n) a

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

State before:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = ↑(Nat.multinomial ∅ n) * hI.dpow (∅.sum n) a
Tactic:
rw [Finset.prod_empty, Finset.sum_empty, hI.dpow_zero ha, Nat.multinomial_empty, Nat.cast_one,
  mul_one]
State after:
no goals

State before:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ∏ i ∈ insert i s, hI.dpow (n i) a = ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a
Tactic:
rw [Finset.prod_insert hi, ih, ← mul_assoc, mul_comm (hI.dpow _ a), mul_assoc,
  hI.dpow_mul _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
State after:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) * hI.dpow (∑ x ∈ insert i s, n x) a =
    ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a

State before:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) * hI.dpow (∑ x ∈ insert i s, n x) a =
    ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a
Tactic:
apply congr_arg₂ _ _ rfl
State after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) = ↑(Nat.multinomial (insert i s) n)

State before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) = ↑(Nat.multinomial (insert i s) n)
Tactic:
rw [mul_comm, Nat.multinomial_insert hi, Finset.sum_insert hi, Nat.cast_mul]
State after:
no goals