Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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]
Proof 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