Theorem: DividedPowers.mul_dpow (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:
classical
induction s using Finset.induction with
| empty =>
  simp only [prod_empty, Nat.multinomial_empty, Nat.cast_one, sum_empty, one_mul]
  rw [hI.dpow_zero ha]
| insert hi hrec =>
  rw [Finset.prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
    mul_assoc, dpow_mul _ _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
  apply congr_arg₂ _ _ rfl
  rw [Nat.multinomial_insert hi, mul_comm, Nat.cast_mul, Finset.sum_insert hi]
State after:
no goals

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
| empty =>
  simp only [prod_empty, Nat.multinomial_empty, Nat.cast_one, sum_empty, one_mul]
  rw [hI.dpow_zero ha]
| insert hi hrec =>
  rw [Finset.prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
    mul_assoc, dpow_mul _ _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
  apply congr_arg₂ _ _ rfl
  rw [Nat.multinomial_insert hi, mul_comm, Nat.cast_mul, Finset.sum_insert hi]
State after:
no goals

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:
simp only [prod_empty, Nat.multinomial_empty, Nat.cast_one, sum_empty, one_mul]
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
⊢ 1 = hI.dpow 0 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
⊢ 1 = hI.dpow 0 a
Tactic:
rw [hI.dpow_zero ha]
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
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ∏ i ∈ insert a✝ s✝, hI.dpow (n i) a = ↑(Nat.multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ s✝).sum n) a
Tactic:
rw [Finset.prod_insert hi, hrec, ← mul_assoc, mul_comm (hI.dpow (n _) a),
  mul_assoc, 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
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * hI.dpow (∑ x ∈ insert a✝ s✝, n x) a =
    ↑(Nat.multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ 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
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) * hI.dpow (∑ x ∈ insert a✝ s✝, n x) a =
    ↑(Nat.multinomial (insert a✝ s✝) n) * hI.dpow ((insert a✝ 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
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(Nat.multinomial (insert a✝ 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
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
hrec : ∏ i ∈ s✝, hI.dpow (n i) a = ↑(Nat.multinomial s✝ n) * hI.dpow (s✝.sum n) a
⊢ ↑(Nat.multinomial s✝ n) * ↑((∑ x ∈ insert a✝ s✝, n x).choose (n a✝)) = ↑(Nat.multinomial (insert a✝ s✝) n)
Tactic:
rw [Nat.multinomial_insert hi, mul_comm, Nat.cast_mul, Finset.sum_insert hi]
State after:
no goals