Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
L1 :
  ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
L4 :
  ∀ p ∈ range (m * n + 1),
    ∑ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
        ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
      ∑ k ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
        (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
                ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
              ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
            hI.dpow p a *
          hJ.dpow (m * n - p) b
⊢ ∑ j ∈ range (m * n + 1),
      ∑ i ∈ filter (fun i => φ i = j) ((range (n + 1)).sym m),
        ∏ i_1 ∈ range (n + 1), dpow hI hJ (Multiset.count i_1 ↑i) (hI.dpow i_1 a * hJ.dpow (n - i_1) b) =
    ∑ 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
Tactic:
rw [Finset.sum_congr rfl L4]
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
L1 :
  ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
L4 :
  ∀ p ∈ range (m * n + 1),
    ∑ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
        ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
      ∑ k ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
        (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
                ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
              ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
            hI.dpow p a *
          hJ.dpow (m * n - p) b
⊢ ∑ x ∈ range (m * n + 1),
      ∑ k ∈ filter (fun x_1 => (fun k => φ k) x_1 = x) ((range (n + 1)).sym m),
        (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
                ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
              ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
            hI.dpow x a *
          hJ.dpow (m * n - x) b =
    ∑ 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