Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ∑ x ∈ range (m * n + 1),
      (↑(m * n - x).factorial)⁻¹ *
        ((↑x.factorial)⁻¹ *
          (↑(m * n).factorial *
            coeff
              (↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = x) ((range (n + 1)).sym m),
                    ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                        Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                      Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
                X ^ x)
              p)) =
    ↑((∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
          (∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
            ((Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
              Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i))) *
        (m * n).choose p)
Tactic:
rw [Finset.sum_eq_single p]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n - p).factorial)⁻¹ *
      ((↑p.factorial)⁻¹ *
        (↑(m * n).factorial *
          coeff
            (↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
                  ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                      Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                    Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
              X ^ p)
            p)) =
    ↑((∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
          (∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
            ((Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
              Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i))) *
        (m * n).choose p)

case a.h₀
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ∀ b ∈ range (m * n + 1),
    b ≠ p →
      (↑(m * n - b).factorial)⁻¹ *
          ((↑b.factorial)⁻¹ *
            (↑(m * n).factorial *
              coeff
                (↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = b) ((range (n + 1)).sym m),
                      ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                          Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                        Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
                  X ^ b)
                p)) =
        0

case a.h₁
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ p ∉ range (m * n + 1) →
    (↑(m * n - p).factorial)⁻¹ *
        ((↑p.factorial)⁻¹ *
          (↑(m * n).factorial *
            coeff
              (↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
                    ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                        Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                      Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
                X ^ p)
              p)) =
      0