Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs (DividedPowers/IdealAdd.lean)

State before:
A : Type ?u.93141
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
⊢ mchoose m n =
    ∑ 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))
Tactic:
rw [← mul_left_inj' (pos_iff_ne_zero.mp (Nat.choose_pos hp))]
State after:
A : Type ?u.93141
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
⊢ mchoose m n * (m * n).choose 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

State before:
A : Type ?u.93141
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
⊢ mchoose m n * (m * n).choose 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:
apply @Nat.cast_injective ℚ
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
⊢ ↑(mchoose m n * (m * n).choose 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)

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
⊢ ↑(mchoose m n * (m * n).choose 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 [Sym.mem_coe, mem_sym_iff, mem_range, ge_iff_le,
  Nat.cast_sum, Nat.cast_mul, Nat.cast_prod, Nat.cast_eq_zero]
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
⊢ ↑(mchoose m n) * ↑((m * n).choose 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)

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
⊢ ↑(mchoose m n) * ↑((m * n).choose 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:
conv_lhs => rw [← Polynomial.coeff_X_add_one_pow ℚ (m * n) p]
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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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:
let A := ℚ[X]
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]
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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]
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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:
let I : Ideal A := ⊤
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 := ⊤
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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 := ⊤
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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:
let hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
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 ⊤
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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 ⊤
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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:
let hII : ∀ (n : ℕ) (a : A), a ∈ I ⊓ I → hI.dpow n a = hI.dpow n a := fun n a _ => rfl
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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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:
let h1 : (1 : A) ∈ I := Submodule.mem_top
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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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:
let hX : X ∈ I := Submodule.mem_top
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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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)

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
⊢ ↑(mchoose m n) * ((X + 1) ^ (m * n)).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 [← hI.factorial_mul_dpow_eq_pow (m * n) (X + 1) Submodule.mem_top]
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
⊢ ↑(mchoose m n) * coeff (↑(m * n).factorial * hI.dpow (m * n) (X + 1)) 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)

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
⊢ ↑(mchoose m n) * coeff (↑(m * n).factorial * hI.dpow (m * n) (X + 1)) 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 [← Polynomial.coeff_C_mul]
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 ↑(mchoose m n) * (↑(m * n).factorial * hI.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)

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 ↑(mchoose m n) * (↑(m * n).factorial * hI.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:
rw [← mul_assoc, mul_comm (C ((mchoose m n) : ℚ)), mul_assoc]
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 * (C ↑(mchoose m n) * hI.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)

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 * (C ↑(mchoose m n) * hI.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 [C_eq_natCast]
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 * (↑(mchoose m n) * hI.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)

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 * (↑(mchoose m n) * hI.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:
rw [← hI.dpow_comp m hn Submodule.mem_top]
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 * 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)

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]
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)

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]
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)

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]
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)

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]
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)

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]
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)

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]
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)

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]
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)

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]
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)

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]
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)

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]
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

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 - 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)
Tactic:
conv_lhs =>
  rw [coeff_natCast_mul, coeff_X_pow, if_pos, mul_one]
  simp only [← Nat.cast_sum, ← Nat.cast_mul, ← Nat.cast_prod]
  rw [← mul_assoc, mul_comm]
  rw [Nat.cast_mul]
  simp only [mul_assoc]
  rw [mul_comm]
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 ∈ 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
      ↑(m * n).factorial =
    ↑((∑ 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)

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 ∈ 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
      ↑(m * n).factorial =
    ↑((∑ 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_sum, Nat.cast_mul, Nat.cast_prod]
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 ∈ 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
      ↑(m * n).factorial =
    (∑ 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)

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 ∈ 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
      ↑(m * n).factorial =
    (∑ 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_mul]
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 ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
      (∏ i_1 ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i_1 ↑i)) *
            (↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * i_1) *
              ↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * (n - i_1))) *
          ((↑(m * n - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
        ↑(m * n).factorial =
    ∑ i ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
      (∏ i_1 ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i_1 ↑i)) *
          (↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * i_1) *
            ↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * (n - i_1))) *
        ↑((m * n).choose p)

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 ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
      (∏ i_1 ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i_1 ↑i)) *
            (↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * i_1) *
              ↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * (n - i_1))) *
          ((↑(m * n - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
        ↑(m * n).factorial =
    ∑ i ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
      (∏ i_1 ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i_1 ↑i)) *
          (↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * i_1) *
            ↑(Nat.multinomial (range (n + 1)) fun i_1 => Multiset.count i_1 ↑i * (n - i_1))) *
        ↑((m * n).choose p)
Tactic:
apply Finset.sum_congr rfl
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 ∈ 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
        ↑(m * n).factorial =
      (∏ 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)

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 ∈ 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
        ↑(m * n).factorial =
      (∏ 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:
intro x _
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 : Sym ℕ m
a✝ : 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
      ↑(m * n).factorial =
    (∏ 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)

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 : Sym ℕ m
a✝ : 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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹) *
      ↑(m * n).factorial =
    (∏ 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 [mul_assoc]
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 : Sym ℕ m
a✝ : 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 - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial)))) =
    (∏ 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)))

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 : Sym ℕ m
a✝ : 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 - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial)))) =
    (∏ 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:
congr
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑(m * n - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑(m * n - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)
Tactic:
ring_nf
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑(m * n - p).factorial)⁻¹ * (↑p.factorial)⁻¹ * ↑(m * n).factorial = ↑((m * n).choose p)

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑(m * n - p).factorial)⁻¹ * (↑p.factorial)⁻¹ * ↑(m * n).factorial = ↑((m * n).choose p)
Tactic:
simp only [mul_assoc]
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑(m * n - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑(m * n - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)
Tactic:
rw [inv_mul_eq_iff_eq_mul₀]
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑p.factorial)⁻¹ * ↑(m * n).factorial = ↑(m * n - p).factorial * ↑((m * n).choose p)

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ (↑p.factorial)⁻¹ * ↑(m * n).factorial = ↑(m * n - p).factorial * ↑((m * n).choose p)

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0
Tactic:
rw [inv_mul_eq_iff_eq_mul₀]
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n).factorial = ↑p.factorial * (↑(m * n - p).factorial * ↑((m * n).choose p))

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n).factorial = ↑p.factorial * (↑(m * n - p).factorial * ↑((m * n).choose p))

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0
Tactic:
rw [← Nat.choose_mul_factorial_mul_factorial hp]
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑((m * n).choose p * p.factorial * (m * n - p).factorial) =
    ↑p.factorial * (↑(m * n - p).factorial * ↑((m * n).choose p))

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑((m * n).choose p * p.factorial * (m * n - p).factorial) =
    ↑p.factorial * (↑(m * n - p).factorial * ↑((m * n).choose p))

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0
Tactic:
simp only [Nat.cast_mul]
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑((m * n).choose p) * ↑p.factorial * ↑(m * n - p).factorial =
    ↑p.factorial * (↑(m * n - p).factorial * ↑((m * n).choose p))

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑((m * n).choose p) * ↑p.factorial * ↑(m * n - p).factorial =
    ↑p.factorial * (↑(m * n - p).factorial * ↑((m * n).choose p))

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0
Tactic:
ring
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑p.factorial ≠ 0

case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0
Tactic:
all_goals
  simp only [ne_eq, Nat.cast_eq_zero]
  apply Nat.factorial_ne_zero
State after:
no goals

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ↑(m * n - p).factorial ≠ 0
Tactic:
simp only [ne_eq, Nat.cast_eq_zero]
State after:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ¬(m * n - p).factorial = 0

State before:
case a.e_a.e_a.e_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 : Sym ℕ m
a✝ : x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m)
⊢ ¬(m * n - p).factorial = 0
Tactic:
apply Nat.factorial_ne_zero
State after:
no goals

State before:
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
Tactic:
intro b _ hb
State after:
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 : ℕ
a✝ : b ∈ range (m * n + 1)
hb : 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

State before:
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 : ℕ
a✝ : b ∈ range (m * n + 1)
hb : 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
Tactic:
rw [coeff_natCast_mul, coeff_X_pow, if_neg hb.symm]
State after:
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 : ℕ
a✝ : b ∈ range (m * n + 1)
hb : b ≠ p
⊢ (↑(m * n - b).factorial)⁻¹ *
      ((↑b.factorial)⁻¹ *
        (↑(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)) *
            0))) =
    0

State before:
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 : ℕ
a✝ : b ∈ range (m * n + 1)
hb : b ≠ p
⊢ (↑(m * n - b).factorial)⁻¹ *
      ((↑b.factorial)⁻¹ *
        (↑(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)) *
            0))) =
    0
Tactic:
simp only [mul_zero]
State after:
no goals

State before:
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
Tactic:
intro hp'
State after:
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
hp' : 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

State before:
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
hp' : 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
Tactic:
simp only [mem_range, Nat.lt_succ_iff] at hp'
State after:
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
hp' : ¬p ≤ m * n
⊢ (↑(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

State before:
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
hp' : ¬p ≤ m * n
⊢ (↑(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
Tactic:
contradiction
State after:
no goals