internlm/Lean-Github huggingface dataset:
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_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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ (fun m x => Sym.fill a m.fst m.snd) m hm ∈ (insert a s).sym n
Tactic:
rw [mem_sym_iff]
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 ι
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ ∀ a_1 ∈ (fun m x => Sym.fill a m.fst m.snd) m hm, a_1 ∈ insert a s
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_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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ ∀ a_1 ∈ (fun m x => Sym.fill a m.fst m.snd) m hm, a_1 ∈ insert a s
Tactic:
intro i hi
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 ι
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : i ∈ (fun m x => Sym.fill a m.fst m.snd) m hm
⊢ i ∈ insert a s
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_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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : i ∈ (fun m x => Sym.fill a m.fst m.snd) m hm
⊢ i ∈ insert a s
Tactic:
rw [Sym.mem_fill_iff] at hi
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 ι
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a ∨ i ∈ m.snd
⊢ i ∈ insert a s
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_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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a ∨ i ∈ m.snd
⊢ i ∈ insert a s
Tactic:
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)
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case inl
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a
⊢ i ∈ insert a s
Tactic:
rw [hi.2]
Proof state after:
case inl
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a
⊢ a ∈ insert a s
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case inl
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : ↑m.fst ≠ 0 ∧ i = a
⊢ a ∈ insert a s
Tactic:
apply mem_insert_self
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case inr
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
i : ι
hi : i ∈ m.snd
⊢ i ∈ insert a s
Tactic:
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
Proof state after:
case inr
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
i : ι
hi : i ∈ m.snd
hm : ∀ a ∈ m.snd, a ∈ s
⊢ i ∈ insert a s
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case inr
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 : (i : Fin (n + 1)) × Sym ι (n - ↑i)
i : ι
hi : i ∈ m.snd
hm : ∀ a ∈ m.snd, a ∈ s
⊢ i ∈ insert a s
Tactic:
exact mem_insert_of_mem (hm i hi)
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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
Tactic:
intro m hm
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 : ℕ
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : m ∈ univ.sigma fun a => s.sym (n - ↑a)
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m
Tactic:
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
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 : ℕ
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : ∀ a ∈ m.snd, a ∈ s
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : (i : Fin (n + 1)) × Sym ι (n - ↑i)
hm : ∀ a ∈ m.snd, a ∈ s
⊢ Sym.filterNe a (Sym.fill a m.fst m.snd) = m
Tactic:
exact Sym.filter_ne_fill a m fun a_1 => ha (hm a a_1)
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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)
Tactic:
intro m hm
Proof state after:
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 : ℕ
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ∏ i ∈ insert a s, dp (Multiset.count i ↑m) (x i) =
    dp (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : Sym ι n
hm : m ∈ (insert a s).sym n
⊢ ∏ i ∈ insert a s, dp (Multiset.count i ↑m) (x i) =
    dp (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
simp only [mem_sym_iff, mem_insert] at hm
Proof state after:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ i ∈ insert a s, dp (Multiset.count i ↑m) (x i) =
    dp (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ i ∈ insert a s, dp (Multiset.count i ↑m) (x i) =
    dp (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
rw [Finset.prod_insert ha]
Proof state after:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dp (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dp (Multiset.count x_1 ↑m) (x x_1) =
    dp (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ dp (Multiset.count a ↑m) (x a) * ∏ x_1 ∈ s, dp (Multiset.count x_1 ↑m) (x x_1) =
    dp (↑(Sym.filterNe a m).fst) (x a) * ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ x_1 ∈ s, dp (Multiset.count x_1 ↑m) (x x_1) = ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∏ x_1 ∈ s, dp (Multiset.count x_1 ↑m) (x x_1) = ∏ i ∈ s, dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply Finset.prod_congr rfl
Proof state after:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∀ x_1 ∈ s, dp (Multiset.count x_1 ↑m) (x x_1) = dp (Multiset.count x_1 ↑(Sym.filterNe a m).snd) (x x_1)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
⊢ ∀ x_1 ∈ s, dp (Multiset.count x_1 ↑m) (x x_1) = dp (Multiset.count x_1 ↑(Sym.filterNe a m).snd) (x x_1)
Tactic:
intro i hi
Proof state after:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ dp (Multiset.count i ↑m) (x i) = dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
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 : ℕ
m : Sym ι n
hm : ∀ a_1 ∈ m, a_1 = a ∨ a_1 ∈ s
i : ι
hi : i ∈ s
⊢ dp (Multiset.count i ↑m) (x i) = dp (Multiset.count i ↑(Sym.filterNe a m).snd) (x i)
Tactic:
apply congr_arg₂ _ _ rfl
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 ι
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 : ∀ 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