-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
M : Type u_2
inst_1 : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst_2 : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hx : ∀ i ∈ s, x i ∈ I) {n : ℕ},
    dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)
hx : ∀ i ∈ Insert.insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
insert :
  ∀ (a_1 : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ)))
    (ha :
      Membership.mem (γ := Finset ((i : Fin n.succ) × Sym ι (n - (↑i : ℕ))))
        (Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦
          s.sym (n - (↑a : ℕ)))
        a_1),
    Sym.filterNe a
        (Sym.fill a (a_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
          (a_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))) =
      a_1
insert₁ :
  ∀ (a_1 : Sym ι n) (ha : a_1 ∈ (Insert.insert a s).sym n),
    ∏ i ∈ Insert.insert a s, dpow (Multiset.count i (↑a_1 : Multiset ι)) (x i) =
      dpow (↑((Sym.filterNe a a_1).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
        ∏ i ∈ s,
          dpow
            (Multiset.count i
              (↑((Sym.filterNe a a_1).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
            (x i)
apply :
  ∀ (m : Sym ι n) (hm : m ∈ (Insert.insert a s).sym n),
    Membership.mem (α :=
      Sym ι
        (n -
          (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
                ((fun (m : Sym ι n) (x : m ∈ (Insert.insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
            ℕ)))
      (γ :=
      Finset
        (Sym ι
          (n -
            (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
                  ((fun (m : Sym ι n) (x : m ∈ (Insert.insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
              ℕ))))
      (s.sym
        (n -
          (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
                ((fun (m : Sym ι n) (x : m ∈ (Insert.insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
            ℕ)))
      (Sigma.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
          ((fun (m : Sym ι n) (x : m ∈ (Insert.insert a s).sym n) ↦ Sym.filterNe a m) m hm) :
        Sym ι
          (n -
            (↑(Sigma.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))
                  ((fun (m : Sym ι n) (x : m ∈ (Insert.insert a s).sym n) ↦ Sym.filterNe a m) m hm)) :
              ℕ)))
⊢ Eq.{u_1 + 1} (α := A)
    (∑ k ∈ (Insert.insert a s).sym n, ∏ i ∈ Insert.insert a s, dpow (Multiset.count i (↑k : Multiset ι)) (x i))
    (∑
      x_1 ∈
        Finset.sigma (α := fun (a : Fin n.succ) ↦ Sym ι (n - (↑a : ℕ))) univ fun (a : Fin n.succ) ↦
          s.sym (n - (↑a : ℕ)),
      dpow (↑(x_1.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
        ∏ i ∈ s,
          dpow (Multiset.count i (↑(x_1.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)) (x i))

Tactic:
apply sum_bij'
      (fun m _ ↦ m.filterNe a)
      (fun m _ ↦ m.2.fill a m.1)
      (fun m hm ↦ mem_sigma.2 ⟨mem_univ _, _⟩)
      (fun m hm ↦ by
        simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]
        simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
        intro b
        apply Or.imp (fun h ↦ h.2) (fun h ↦ hm b h))
      (fun m _ ↦ m.fill_filterNe a)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_sigma, Sigma.fst, And.intro, Finset.sum_bij'