internlm/Lean-Github huggingface dataset:
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).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
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 ≠ 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
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 ≠ 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
Proof state after:
no goals
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 ≠ 0
Tactic:
simp only [ne_eq, Nat.cast_eq_zero]
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 = 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)
⊢ ¬(m * n - p).factorial = 0
Tactic:
apply Nat.factorial_ne_zero
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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]
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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'
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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'
Proof 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
Theorem: DividedPowers.IdealAdd.dpow_comp_coeffs
Proof 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
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
x : A
hn : n ≠ 0
hx : x ∈ I + J
⊢ dpow hI hJ m (dpow hI hJ n x) = ↑(mchoose m n) * dpow hI hJ (m * n) x
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup] at hx
Proof state after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
x : A
hn : n ≠ 0
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ m (dpow hI hJ n x) = ↑(mchoose m n) * dpow hI hJ (m * n) x
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
x : A
hn : n ≠ 0
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ m (dpow hI hJ n x) = ↑(mchoose m n) * dpow hI hJ (m * n) x
Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ m (dpow hI hJ n (a + b)) = ↑(mchoose m n) * dpow hI hJ (m * n) (a + b)
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ m (dpow hI hJ n (a + b)) = ↑(mchoose m n) * dpow hI hJ (m * n) (a + b)
Tactic:
rw [dpow_comp_aux hI hJ hIJ m hn ha hb,
  dpow_add' hI hJ hIJ _ (Submodule.mem_sup_left ha) (Submodule.mem_sup_right hb), Finset.mul_sum]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ 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 a *
        hJ.dpow (m * n - p) b =
    ∑ i ∈ range (m * n + 1), ↑(mchoose m n) * (dpow hI hJ i a * dpow hI hJ (m * n - i) b)
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ 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 a *
        hJ.dpow (m * n - p) b =
    ∑ i ∈ range (m * n + 1), ↑(mchoose m n) * (dpow hI hJ i a * dpow hI hJ (m * n - i) b)
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (m * n + 1),
    ↑(∑ 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)) *
          hI.dpow x a *
        hJ.dpow (m * n - x) b =
      ↑(mchoose m n) * (dpow hI hJ x a * dpow hI hJ (m * n - x) b)
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ x ∈ range (m * n + 1),
    ↑(∑ 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)) *
          hI.dpow x a *
        hJ.dpow (m * n - x) b =
      ↑(mchoose m n) * (dpow hI hJ x a * dpow hI hJ (m * n - x) b)
Tactic:
intro p hp
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : 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 a *
      hJ.dpow (m * n - p) b =
    ↑(mchoose m n) * (dpow hI hJ p a * dpow hI hJ (m * n - p) b)
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : 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 a *
      hJ.dpow (m * n - p) b =
    ↑(mchoose m n) * (dpow hI hJ p a * dpow hI hJ (m * n - p) b)
Tactic:
rw [dpow_eq_of_mem_left hI hJ hIJ _ ha]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : 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 a *
      hJ.dpow (m * n - p) b =
    ↑(mchoose m n) * (hI.dpow p a * dpow hI hJ (m * n - p) b)
Theorem: DividedPowers.IdealAdd.dpow_comp
Proof state before:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : 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 a *
      hJ.dpow (m * n - p) b =
    ↑(mchoose m n) * (hI.dpow p a * dpow hI hJ (m * n - p) b)
Tactic:
rw [dpow_eq_of_mem_right hI hJ hIJ _ hb]
Proof state after:
case intro.intro.intro.intro
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
p : ℕ
hp : 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 a *
      hJ.dpow (m * n - p) b =
    ↑(mchoose m n) * (hI.dpow p a * hJ.dpow (m * n - p) b)