Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case insert.a
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i) =
    ∑ x_1 ∈ univ.sigma fun a => s.sym (n - ↑a), dpow (↑x_1.fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑x_1.snd) (x i)
Tactic:
apply sum_bij'
  (fun m _ => Sym.filterNe a m)
  (fun m _ => m.2.fill a m.1)
  (fun m hm => Finset.mem_sigma.2 ⟨mem_univ _, _⟩)
  (fun m hm => by
    rw [mem_sym_iff]
    intro i hi
    rw [Sym.mem_fill_iff] at hi
    cases hi with
    | inl hi =>
      rw [hi.2]
      exact mem_insert_self a s
    | inr hi =>
      simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
      exact mem_insert_of_mem (hm i hi))
  (fun m _ => Sym.fill_filterNe a _ )
Proof state after:
case insert.a.right_inv
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∀ a_1 ∈ univ.sigma fun a => s.sym (n - ↑a), Sym.filterNe a (Sym.fill a a_1.fst a_1.snd) = a_1

case insert.a.h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∀ a_1 ∈ (insert a s).sym n,
    ∏ i ∈ insert a s, dpow (Multiset.count i ↑a_1) (x i) =
      dpow (↑(Sym.filterNe a a_1).fst) (x a) * ∏ i ∈ s, dpow (Multiset.count i ↑(Sym.filterNe a a_1).snd) (x i)

A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
dpow : ℕ → A → A
dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_2
inst✝ : DecidableEq ι
x : ι → A
dpow_add : ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_3 ∈ range n.succ, dpow x_3 x * dpow (n - x_3) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ (n : ℕ), dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∀ (m : Sym ι n) (hm : m ∈ (insert a s).sym n),
    ((fun m x => Sym.filterNe a m) m hm).snd ∈ s.sym (n - ↑((fun m x => Sym.filterNe a m) m hm).fst)