Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case insert.a
A : Type ?u.63345
inst✝³ : CommSemiring A
I : Ideal A
hI : DividedPowers I
M : Type u_1
D : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring D
dp : ℕ → M → D
dpow_zero : ∀ (x : M), dp 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dp n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ (n : ℕ) (x y : M), dp n (x + y) = ∑ x_1 ∈ range n.succ, dp x_1 x * dp (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (n : ℕ), dp n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dp (Multiset.count i ↑k) (x i)
n : ℕ
⊢ ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dp (Multiset.count i ↑k) (x i) =
    ∑ x_1 ∈ univ.sigma fun a => s.sym (n - ↑a), dp (↑x_1.fst) (x a) * ∏ i ∈ s, dp (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]
        apply mem_insert_self
      | 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.63345
inst✝³ : CommSemiring A
I : Ideal A
hI : DividedPowers I
M : Type u_1
D : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring D
dp : ℕ → M → D
dpow_zero : ∀ (x : M), dp 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dp n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ (n : ℕ) (x y : M), dp n (x + y) = ∑ x_1 ∈ range n.succ, dp x_1 x * dp (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (n : ℕ), dp n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dp (Multiset.count i ↑k) (x i)
n : ℕ
⊢ ∀ 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.63345
inst✝³ : CommSemiring A
I : Ideal A
hI : DividedPowers I
M : Type u_1
D : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring D
dp : ℕ → M → D
dpow_zero : ∀ (x : M), dp 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dp n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ (n : ℕ) (x y : M), dp n (x + y) = ∑ x_1 ∈ range n.succ, dp x_1 x * dp (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (n : ℕ), dp n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dp (Multiset.count i ↑k) (x i)
n : ℕ
⊢ ∀ a_1 ∈ (insert a s).sym n,
    ∏ i ∈ insert a s, dp (Multiset.count i ↑a_1) (x i) =
      dp (↑(Sym.filterNe a a_1).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a a_1).snd) (x i)

A : Type ?u.63345
inst✝³ : CommSemiring A
I : Ideal A
hI : DividedPowers I
M : Type u_1
D : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommSemiring D
dp : ℕ → M → D
dpow_zero : ∀ (x : M), dp 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dp n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ (n : ℕ) (x y : M), dp n (x + y) = ∑ x_1 ∈ range n.succ, dp x_1 x * dp (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (n : ℕ), dp n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dp (Multiset.count i ↑k) (x i)
n : ℕ
⊢ ∀ (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)