internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n - 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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ↑(∑ x ∈ 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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ↑(∑ x ∈ 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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (∑ x ∈ 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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (∑ x ∈ 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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ∑ i ∈ 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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ∑ i ∈ 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
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ∀ x ∈ 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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ ∀ x ∈ 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 _
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
x : 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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
x : 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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
x : 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)))
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
x : 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
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 - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)
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 - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)
Tactic:
ring_nf
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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹ * ↑(m * n).factorial = ↑((m * n).choose p)
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 - p).factorial)⁻¹ * (↑p.factorial)⁻¹ * ↑(m * n).factorial = ↑((m * n).choose p)
Tactic:
simp only [mul_assoc]
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 - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)
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 - p).factorial)⁻¹ * ((↑p.factorial)⁻¹ * ↑(m * n).factorial) = ↑((m * n).choose p)
Tactic:
rw [inv_mul_eq_iff_eq_mul₀]
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)
⊢ (↑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
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)
⊢ (↑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₀]
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).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