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)
⊢ ∑ 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:
suffices L4 :
  ∀ (p : ℕ) (_ : p ∈ Finset.range (m * n + 1)),
    ((Finset.filter (fun x : Sym ℕ m => (fun k : Sym ℕ m => φ k) x = p)
            ((Finset.range (n + 1)).sym m)).sum
        fun x : Sym ℕ m =>
        (Finset.range (n + 1)).prod fun i : ℕ =>
          dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b)) =
      (Finset.filter (fun x : Sym ℕ m => (fun k : Sym ℕ m => φ k) x = p)
            ((Finset.range (n + 1)).sym m)).sum
        fun k : Sym ℕ m =>
        ((Finset.range (n + 1)).prod fun i : ℕ => ↑(cnik n i ↑k)) *
                ↑(Nat.multinomial (Finset.range (n + 1)) fun i : ℕ => Multiset.count i ↑k * i) *
              ↑(Nat.multinomial (Finset.range (n + 1)) fun i : ℕ =>
                  Multiset.count i ↑k * (n - i)) *
            hI.dpow p a *
          hJ.dpow (m * n - p) b by
    rw [Finset.sum_congr rfl L4]
    simp only [Sym.mem_coe, mem_sym_iff, mem_range, ge_iff_le, Nat.cast_sum, Nat.cast_mul,
    Nat.cast_prod]
    simp_rw [Finset.sum_mul]
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)
⊢ ∀ 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