internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
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
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ dpow (Multiset.count i ↑m) (x i) = dpow (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply congr_arg₂ _ _ rfl
Proof state after:
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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i ↑m = Multiset.count i ↑(Sym.filterNe a m).snd
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i ↑m = Multiset.count i ↑(Sym.filterNe a m).snd
Tactic:
conv_lhs => rw [← Sym.fill_filterNe a m, Sym.coe_fill]
Proof state after:
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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i (↑(Sym.filterNe a m).snd + ↑(Sym.replicate (↑(Sym.filterNe a m).fst) a)) =
    Multiset.count i ↑(Sym.filterNe a m).snd
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ Multiset.count i (↑(Sym.filterNe a m).snd + ↑(Sym.replicate (↑(Sym.filterNe a m).fst) a)) =
    Multiset.count i ↑(Sym.filterNe a m).snd
Tactic:
simp only [Multiset.count_add, add_right_eq_self, Multiset.count_eq_zero,
  Sym.mem_coe, Sym.mem_replicate, not_and]
Proof state after:
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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ ↑(Sym.filterNe a m).fst ≠ 0 → ¬i = a
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
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 : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ ↑(Sym.filterNe a m).fst ≠ 0 → ¬i = a
Tactic:
exact fun _ => ne_of_mem_of_not_mem hi ha
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
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)
Tactic:
intro m hm
Proof state after:
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)
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
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)
Tactic:
convert sym_filterNe_mem a hm
Proof state after:
case h.e'_5.h.e'_3
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
⊢ s = (insert a s).erase a
Theorem: DividedPowers.dpow_sum_aux
Proof state before:
case h.e'_5.h.e'_3
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
⊢ s = (insert a s).erase a
Tactic:
rw [erase_insert ha]
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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_add :
  ∀ (n : ℕ) (x y : M),
    dp n (x + y) =
      ∑ x_1 ∈ antidiagonal n,
        match x_1 with
        | (k, l) => dp k x * dp l y
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dp n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
x : ι → M
n : ℕ
⊢ dp n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dp (Multiset.count i ↑k) (x i)
Tactic:
simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add
Proof state after:
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 ι
s : Finset ι
x : ι → M
n : ℕ
dpow_add : ∀ (n : ℕ) (x y : M), dp n (x + y) = ∑ x_1 ∈ range n.succ, dp x_1 x * dp (n - x_1) y
⊢ dp n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case empty
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
n : ℕ
⊢ dp n (∅.sum x) = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
rw [sum_empty]
Proof state after:
case empty
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
n : ℕ
⊢ dp n 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case empty
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
n : ℕ
⊢ dp n 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
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
n : ℕ
hn : n = 0
⊢ dp n 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)

case neg
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
n : ℕ
hn : ¬n = 0
⊢ dp n 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case pos
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
n : ℕ
hn : n = 0
⊢ dp n 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
rw [hn]
Proof state after:
case pos
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
n : ℕ
hn : n = 0
⊢ dp 0 0 = ∑ k ∈ ∅.sym 0, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case pos
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
n : ℕ
hn : n = 0
⊢ dp 0 0 = ∑ k ∈ ∅.sym 0, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
haveI : Unique (Sym ι Nat.zero) := Sym.uniqueZero
Proof state after:
case pos
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
n : ℕ
hn : n = 0
this : Unique (Sym ι Nat.zero)
⊢ dp 0 0 = ∑ k ∈ ∅.sym 0, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case pos
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
n : ℕ
hn : n = 0
this : Unique (Sym ι Nat.zero)
⊢ dp 0 0 = ∑ k ∈ ∅.sym 0, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
rw [dpow_zero, sum_unique_nonempty, prod_empty]
Proof state after:
case pos.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
n : ℕ
hn : n = 0
this : Unique (Sym ι Nat.zero)
⊢ (∅.sym 0).Nonempty
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case pos.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
n : ℕ
hn : n = 0
this : Unique (Sym ι Nat.zero)
⊢ (∅.sym 0).Nonempty
Tactic:
simp only [Nat.zero_eq, sym_zero, singleton_nonempty]
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case neg
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
n : ℕ
hn : ¬n = 0
⊢ dp n 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
rw [dpow_eval_zero hn]
Proof state after:
case neg
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
n : ℕ
hn : ¬n = 0
⊢ 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case neg
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
n : ℕ
hn : ¬n = 0
⊢ 0 = ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i)
Tactic:
apply symm
Proof state after:
case neg.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
n : ℕ
hn : ¬n = 0
⊢ ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i) = 0
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case neg.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
n : ℕ
hn : ¬n = 0
⊢ ∑ k ∈ ∅.sym n, ∏ i ∈ ∅, dp (Multiset.count i ↑k) (x i) = 0
Tactic:
convert Finset.sum_empty
Proof state after:
case h.e'_2.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
n : ℕ
hn : ¬n = 0
⊢ ∅.sym n = ∅
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case h.e'_2.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
n : ℕ
hn : ¬n = 0
⊢ ∅.sym n = ∅
Tactic:
rw [sym_eq_empty]
Proof state after:
case h.e'_2.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
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case h.e'_2.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
n : ℕ
hn : ¬n = 0
⊢ n ≠ 0 ∧ ∅ = ∅
Tactic:
exact ⟨hn, rfl⟩
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case insert
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 : ℕ
⊢ dp n ((insert a s).sum x) = ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dp (Multiset.count i ↑k) (x i)
Tactic:
simp_rw [sum_insert ha, dpow_add n, sum_range, ih, mul_sum, sum_sigma']
Proof state after:
case insert
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 : ℕ
⊢ ∑ 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) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dp (Multiset.count i ↑k) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case insert
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 : ℕ
⊢ ∑ 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) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dp (Multiset.count i ↑k) (x i)
Tactic:
apply symm
Proof state after:
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)