internlm/Lean-Github huggingface dataset:
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
⊢ (↑(m * n).factorial * hI.dpow m (hI.dpow n (X + 1))).coeff 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 [← dpow_eq_of_mem_left hI hI hII n Submodule.mem_top,
  ← dpow_eq_of_mem_left hI hI hII m Submodule.mem_top]
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).factorial * dpow hI hI m (dpow hI hI n (X + 1))).coeff 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)
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
⊢ (↑(m * n).factorial * dpow hI hI m (dpow hI hI n (X + 1))).coeff 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 [dpow_comp_aux hI hI hII m hn hX h1]
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).factorial *
          ∑ p ∈ range (m * n + 1),
            ↑(∑ 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)) *
                hI.dpow p X *
              hI.dpow (m * n - p) 1).coeff
      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)
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
⊢ (↑(m * n).factorial *
          ∑ p ∈ range (m * n + 1),
            ↑(∑ 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)) *
                hI.dpow p X *
              hI.dpow (m * n - p) 1).coeff
      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 [← C_eq_natCast]
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
⊢ (C ↑(m * n).factorial *
          ∑ p ∈ range (m * n + 1),
            ↑(∑ 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)) *
                hI.dpow p X *
              hI.dpow (m * n - p) 1).coeff
      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)
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
⊢ (C ↑(m * n).factorial *
          ∑ p ∈ range (m * n + 1),
            ↑(∑ 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)) *
                hI.dpow p X *
              hI.dpow (m * n - p) 1).coeff
      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:
simp only [Finset.mul_sum]
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
⊢ (∑ i ∈ range (m * n + 1),
          C ↑(m * n).factorial *
            (↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = i) ((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)) *
                hI.dpow i X *
              hI.dpow (m * n - i) 1)).coeff
      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)
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
⊢ (∑ i ∈ range (m * n + 1),
          C ↑(m * n).factorial *
            (↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = i) ((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)) *
                hI.dpow i X *
              hI.dpow (m * n - i) 1)).coeff
      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:
simp only [finset_sum_coeff]
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
⊢ ∑ b ∈ range (m * n + 1),
      (C ↑(m * n).factorial *
            (↑(∑ 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)) *
                hI.dpow b X *
              hI.dpow (m * n - b) 1)).coeff
        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)
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
⊢ ∑ b ∈ range (m * n + 1),
      (C ↑(m * n).factorial *
            (↑(∑ 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)) *
                hI.dpow b X *
              hI.dpow (m * n - b) 1)).coeff
        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:
simp only [hI]
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
⊢ ∑ x ∈ range (m * n + 1),
      (C ↑(m * n).factorial *
            (↑(∑ 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)) *
                (RatAlgebra.dividedPowers ⊤).dpow x X *
              (RatAlgebra.dividedPowers ⊤).dpow (m * n - x) 1)).coeff
        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)
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),
      (C ↑(m * n).factorial *
            (↑(∑ 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)) *
                (RatAlgebra.dividedPowers ⊤).dpow x X *
              (RatAlgebra.dividedPowers ⊤).dpow (m * n - x) 1)).coeff
        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:
simp only [RatAlgebra.dpow_eq_inv_fact_smul _ _ Submodule.mem_top]
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
⊢ ∑ x ∈ range (m * n + 1),
      (C ↑(m * n).factorial *
            (↑(∑ 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)) *
                Ring.inverse ↑x.factorial • X ^ x *
              Ring.inverse ↑(m * n - x).factorial • 1 ^ (m * n - x))).coeff
        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)
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),
      (C ↑(m * n).factorial *
            (↑(∑ 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)) *
                Ring.inverse ↑x.factorial • X ^ x *
              Ring.inverse ↑(m * n - x).factorial • 1 ^ (m * n - x))).coeff
        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:
simp only [map_natCast, Nat.cast_sum, Nat.cast_mul, Nat.cast_prod,
  Ring.inverse_eq_inv', Algebra.mul_smul_comm, one_pow, mul_one, coeff_smul,
  coeff_natCast_mul, smul_eq_mul]
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
⊢ ∑ 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)
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:
simp only [← Nat.cast_prod, ← Nat.cast_mul, ← Nat.cast_sum]
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
⊢ ∑ 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)