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

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

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

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

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

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

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

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

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 * hJ.dpow (m * n - p) b)
Tactic:
simp only [mul_assoc]
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)

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 : ℕ
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))) =
    ↑(mchoose m n)
Tactic:
rw [dpow_comp_coeffs hn (Nat.lt_succ_iff.mp (Finset.mem_range.mp hp))]
State after:
no goals