awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : n = 0
pos : Eq.{u_1 + 1} (α := A) 1 (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)
⊢ dpow 0 0 = (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)

Tactic:
rw [dpow_zero I.zero_mem]

Premises used: AddSubmonoid.zero_mem
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : n = 0
⊢ Eq.{u_1 + 1} (α := A) 1 (↑(card.{u_3} (α := Sym ι 0) (Finset.sym ∅ 0)) : A)

Tactic:
simp only [sym_zero, card_singleton, cast_one]

Premises used: Finset.sym_zero, Nat.cast_one, Finset.card_singleton
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
neg : Eq.{u_1 + 1} (α := A) (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A) (↑0 : A)
⊢ dpow n 0 = (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A)

Tactic:
rw [dpow_eval_zero hn, eq_comm, ← cast_zero]

Premises used: eq_comm, Nat.cast_zero
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
neg : card.{u_3} (α := Sym ι n) (Finset.sym ∅ n) = 0
⊢ Eq.{u_1 + 1} (α := A) (↑(card.{u_3} (α := Sym ι n) (Finset.sym ∅ n)) : A) (↑0 : A)

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
neg : n ≠ 0 ∧ Eq.{u_3 + 1} (α := Finset ι) ∅ ∅
⊢ card.{u_3} (α := Sym ι n) (Finset.sym ∅ n) = 0

Tactic:
rw [card_eq_zero, sym_eq_empty]

Premises used: Finset.sym_eq_empty, Finset.card_eq_zero
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ Eq.{u_3 + 1} (α := Finset ι) ∅ ∅

Tactic:
⟨hn, rfl⟩

Premises used: And.intro, rfl
-- 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
hx : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ Eq.{u_3 + 1} (α := Finset ι) ∅ ∅

Tactic:
exact ⟨hn, rfl⟩
-- 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 a s, x i ∈ I
n : ℕ
⊢ ∀ i ∈ s, x i ∈ I

Tactic:
have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
-- 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 :
  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))
⊢ dpow n ((Insert.insert a s).sum x) =
    ∑ k ∈ (Insert.insert a s).sym n, ∏ i ∈ Insert.insert a s, dpow (Multiset.count i (↑k : Multiset ι)) (x i)

Tactic:
simp_rw [sum_insert ha,
      dpow_add (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i),
      sum_range, ih hx', mul_sum, sum_sigma', eq_comm]

Premises used: Finset.mul_sum, Finset.mem_insert_self, eq_comm, Finset.sum_sigma', Finset.sum_range, AddSubmonoid.sum_mem, Finset.sum_insert
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm :
  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 : ℕ))) m
simp :
  ∀ (a_1 : ι),
    (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ a_1 = a ∨
        a_1 ∈ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))) →
      a_1 = a ∨ a_1 ∈ s
⊢ (fun (m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ)))
          (x :
            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 : ℕ)))
              m) ↦
        Sym.fill a (m.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
          (m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))))
      m hm ∈
    (insert a s).sym n

Tactic:
simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]

Premises used: Finset.mem_sym_iff, Nat.succ_eq_add_one, Sym.mem_fill_iff, Finset.mem_insert
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm :
  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 : ℕ))) m
⊢ ∀ a ∈ m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))), a ∈ s

Tactic:
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm

Premises used: Finset.mem_univ, Finset.mem_sym_iff, Finset.mem_sigma, true_and
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm : ∀ a ∈ m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))), a ∈ s
b : ι
⊢ (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ b = a ∨
      b ∈ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))) →
    b = a ∨ b ∈ s

Tactic:
apply Or.imp (fun h ↦ h.2) (fun h ↦ hm b h)

Premises used: Or.imp
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm : ∀ a ∈ m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))), a ∈ s
⊢ Sym.filterNe a
      (Sym.fill a (m.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
        (m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))) =
    m

Tactic:
Sym.filter_ne_fill a m fun a_1 ↦ ha (hm a a_1)

Premises used: Sym.filter_ne_fill
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : (i : Fin n.succ) × Sym ι (n - (↑i : ℕ))
hm : ∀ a ∈ m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))), a ∈ s
⊢ Sym.filterNe a
      (Sym.fill a (m.fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))
        (m.snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ))))) =
    m

Tactic:
exact Sym.filter_ne_fill a m fun a_1 ↦ ha (hm a a_1)

Premises used: Sym.filter_ne_fill
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s

Tactic:
simp only [mem_sym_iff, mem_insert] at hm

Premises used: Finset.mem_sym_iff, Finset.mem_insert
-- 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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
insert :
  dpow (Multiset.count a (↑m : Multiset ι)) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1) =
    dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)
⊢ ∏ i ∈ Insert.insert a s, dpow (Multiset.count i (↑m : Multiset ι)) (x i) =
    dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)

Tactic:
rw [prod_insert ha]

Premises used: Finset.prod_insert
-- 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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
insert :
  Eq.{u_1 + 1} (α := A) (∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1))
    (∏ i ∈ s,
      dpow
        (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
        (x i))
⊢ dpow (Multiset.count a (↑m : Multiset ι)) (x a) * ∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1) =
    dpow (↑((Sym.filterNe a m).fst (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : ℕ) (x a) *
      ∏ i ∈ s,
        dpow
          (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
          (x i)

Tactic:
apply congr_arg₂ _ rfl

Premises used: rfl, congr_arg₂
-- 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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
insert :
  ∀ x_1 ∈ s,
    dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1) =
      dpow
        (Multiset.count x_1 (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
        (x x_1)
⊢ Eq.{u_1 + 1} (α := A) (∏ x_1 ∈ s, dpow (Multiset.count x_1 (↑m : Multiset ι)) (x x_1))
    (∏ i ∈ s,
      dpow
        (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
        (x i))

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
apply :
  Multiset.count i (↑m : Multiset ι) =
    Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)
⊢ dpow (Multiset.count i (↑m : Multiset ι)) (x i) =
    dpow (Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι))
      (x i)

Tactic:
apply congr_arg₂ _ _ rfl

Premises used: rfl, congr_arg₂
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
rw :
  Multiset.count i
    (↑(Sym.fill a ((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))
          ((Sym.filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))) :
      Multiset ι)
| Multiset.count i (↑m : Multiset ι)

Tactic:
rw [← m.fill_filterNe a]

Premises used: Sym.fill_filterNe
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
conv_lhs :
  Multiset.count i
      (↑(Sym.fill a ((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))
            ((Sym.filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))) :
        Multiset ι) =
    Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)
⊢ Multiset.count i (↑m : Multiset ι) =
    Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)

Tactic:
conv_lhs => rw [← m.fill_filterNe a]

Premises used: Sym.fill_filterNe
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i
      (↑(Sym.fill a ((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))
            ((Sym.filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))) :
        Multiset ι) =
    Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)

Tactic:
Sym.count_coe_fill_of_ne (ne_of_mem_of_not_mem hi ha)

Premises used: Sym.count_coe_fill_of_ne, ne_of_mem_of_not_mem
-- 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 a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i
      (↑(Sym.fill a ((Sym.filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))
            ((Sym.filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym ι (n - (↑i : ℕ))))) :
        Multiset ι) =
    Multiset.count i (↑((Sym.filterNe a m).snd (β := fun (i : Fin n.succ) ↦ Sym ι (n - (↑i : ℕ)))) : Multiset ι)

Tactic:
exact Sym.count_coe_fill_of_ne (ne_of_mem_of_not_mem hi ha)

Premises used: Sym.count_coe_fill_of_ne, ne_of_mem_of_not_mem