internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = 1
Tactic:
convert congr_arg₂ coeff hb rfl
Proof state after:
case h.e'_2
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = (C a * b).coeff ?h

case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 ?h

case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ℕ
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case h.e'_2
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ a * b.coeff 0 = (C a * b).coeff ?h

case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 ?h

case h
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ ℕ
Tactic:
rw [Polynomial.coeff_C_mul]
Proof state after:
case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 0
Theorem: DividedPowers.IdealAdd.Polynomial.inv_C_eq_C_inv
Proof state before:
case h.e'_3
A : Type ?u.83499
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
R : Type u_1
inst✝ : CommSemiring R
a : R
ha : ¬IsUnit a
b : R[X]
hb : C a * b = 1
⊢ 1 = coeff 1 0
Tactic:
simp only [coeff_one_zero]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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))]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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 ℚ
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
⊢ ↑(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)
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
⊢ ↑(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]
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
⊢ ↑(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)
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
⊢ ↑(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]
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
⊢ ↑(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)
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
⊢ ↑(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]
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]
⊢ ↑(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)
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]
⊢ ↑(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 := ⊤
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 := ⊤
⊢ ↑(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)
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 := ⊤
⊢ ↑(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 ⊤
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 ⊤
⊢ ↑(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)
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 ⊤
⊢ ↑(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
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
⊢ ↑(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)
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
⊢ ↑(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
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
⊢ ↑(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)
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
⊢ ↑(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
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
⊢ ↑(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)
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
⊢ ↑(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]
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
⊢ ↑(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)
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
⊢ ↑(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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (C ↑(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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (C ↑(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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n).factorial * (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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n).factorial * (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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n).factorial * (↑(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)
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof state before:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n).factorial * (↑(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]
Proof state after:
case a
A✝ : Type ?u.93141
inst✝ : CommRing A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
m n p : ℕ
hn : n ≠ 0
hp : p ≤ m * n
A : Type := ℚ[X]
I : Ideal A := ⊤
hI : DividedPowers I := RatAlgebra.dividedPowers ⊤
hII : ∀ (n : ℕ), ∀ a ∈ I ⊓ I, hI.dpow n a = hI.dpow n a := fun n a x => rfl
h1 : 1 ∈ I := Submodule.mem_top
hX : X ∈ I := Submodule.mem_top
⊢ (↑(m * n).factorial * 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)