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 : 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.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 (↑(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.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 (↑(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.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
⊢ ↑(Sym.filterNe a m).fst ≠ 0 → ¬i = a
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 : 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.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)
Tactic:
intro m hm
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 : 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.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)
Tactic:
convert sym_filterNe_mem a hm
Proof state after:
case h.e'_5.h.e'_3
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
⊢ s = (insert a s).erase a
Theorem: DividedPowers.dpow_sum_aux'
Proof state before:
case h.e'_5.h.e'_3
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
⊢ s = (insert a s).erase a
Tactic:
rw [erase_insert ha]
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum
Proof state before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ (n : ℕ), hI.dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, hI.dpow (Multiset.count i ↑k) (x i)
Tactic:
refine' dpow_sum_aux hI.dpow _ ?_ _ hx
Proof state after:
case refine'_1
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ {x : A}, x ∈ I → hI.dpow 0 x = 1

case refine'_2
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → hI.dpow n (x + y) = ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y

case refine'_3
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ {n : ℕ}, n ≠ 0 → hI.dpow n 0 = 0
Theorem: DividedPowers.dpow_sum
Proof state before:
case refine'_1
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ {x : A}, x ∈ I → hI.dpow 0 x = 1
Tactic:
intro x
Proof state after:
case refine'_1
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ι → A
hx : ∀ i ∈ s, x✝ i ∈ I
x : A
⊢ x ∈ I → hI.dpow 0 x = 1
Theorem: DividedPowers.dpow_sum
Proof state before:
case refine'_1
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ι → A
hx : ∀ i ∈ s, x✝ i ∈ I
x : A
⊢ x ∈ I → hI.dpow 0 x = 1
Tactic:
exact hI.dpow_zero
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum
Proof state before:
case refine'_2
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ (n : ℕ) {x y : A}, x ∈ I → y ∈ I → hI.dpow n (x + y) = ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y
Tactic:
intro n x y hx hy
Proof state after:
case refine'_2
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ι → A
hx✝ : ∀ i ∈ s, x✝ i ∈ I
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ hI.dpow n (x + y) = ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y
Theorem: DividedPowers.dpow_sum
Proof state before:
case refine'_2
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ι → A
hx✝ : ∀ i ∈ s, x✝ i ∈ I
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ hI.dpow n (x + y) = ∑ k ∈ antidiagonal n, hI.dpow k.1 x * hI.dpow k.2 y
Tactic:
rw [hI.dpow_add n hx hy,
  Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun k l ↦ hI.dpow k x * hI.dpow l y)]
Proof state after:
no goals
Theorem: DividedPowers.dpow_sum
Proof state before:
case refine'_3
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
⊢ ∀ {n : ℕ}, n ≠ 0 → hI.dpow n 0 = 0
Tactic:
intro n hn
Proof state after:
case refine'_3
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Theorem: DividedPowers.dpow_sum
Proof state before:
case refine'_3
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
x : ι → A
hx : ∀ i ∈ s, x i ∈ I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Tactic:
exact hI.dpow_eval_zero hn
Proof state after:
no goals
Theorem: DividedPowers.prod_dpow_self
Proof state before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
s : Finset ι
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
Tactic:
induction' s using Finset.induction with i s hi ih
Proof state after:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = ↑(Nat.multinomial ∅ n) * hI.dpow (∅.sum n) a

case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ∏ i ∈ insert i s, hI.dpow (n i) a = ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a
Theorem: DividedPowers.prod_dpow_self
Proof state before:
case empty
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
⊢ ∏ i ∈ ∅, hI.dpow (n i) a = ↑(Nat.multinomial ∅ n) * hI.dpow (∅.sum n) a
Tactic:
rw [Finset.prod_empty, Finset.sum_empty, hI.dpow_zero ha, Nat.multinomial_empty, Nat.cast_one,
  mul_one]
Proof state after:
no goals
Theorem: DividedPowers.prod_dpow_self
Proof state before:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ∏ i ∈ insert i s, hI.dpow (n i) a = ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a
Tactic:
rw [Finset.prod_insert hi, ih, ← mul_assoc, mul_comm (hI.dpow _ a), mul_assoc,
  hI.dpow_mul _ _ ha, ← Finset.sum_insert hi, ← mul_assoc]
Proof state after:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) * hI.dpow (∑ x ∈ insert i s, n x) a =
    ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a
Theorem: DividedPowers.prod_dpow_self
Proof state before:
case insert
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) * hI.dpow (∑ x ∈ insert i s, n x) a =
    ↑(Nat.multinomial (insert i s) n) * hI.dpow ((insert i s).sum n) a
Tactic:
apply congr_arg₂ _ _ rfl
Proof state after:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) = ↑(Nat.multinomial (insert i s) n)
Theorem: DividedPowers.prod_dpow_self
Proof state before:
A : Type u_2
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_1
n : ι → ℕ
a : A
ha : a ∈ I
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, hI.dpow (n i) a = ↑(Nat.multinomial s n) * hI.dpow (s.sum n) a
⊢ ↑(Nat.multinomial s n) * ↑((∑ x ∈ insert i s, n x).choose (n i)) = ↑(Nat.multinomial (insert i s) n)
Tactic:
rw [mul_comm, Nat.multinomial_insert hi, Finset.sum_insert hi, Nat.cast_mul]
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ MvPolynomial.coeff d ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Tactic:
rw [Commute.add_pow' (Commute.all _ _), MvPolynomial.coeff_sum]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ ∑ x ∈ Finset.antidiagonal n, MvPolynomial.coeff d (n.choose x.1 • (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2)) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ ∑ x ∈ Finset.antidiagonal n, MvPolynomial.coeff d (n.choose x.1 • (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2)) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Tactic:
simp only [nsmul_eq_smul, MvPolynomial.coeff_smul]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ ∑ x ∈ Finset.antidiagonal n, n.choose x.1 • MvPolynomial.coeff d (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ ∑ x ∈ Finset.antidiagonal n, n.choose x.1 • MvPolynomial.coeff d (MvPolynomial.X 0 ^ x.1 * MvPolynomial.X 1 ^ x.2) =
    ↑(if (d 0, d 1) ∈ Finset.antidiagonal n then n.choose (d 0) else 0)
Tactic:
simp only [Fin.isValue, Nat.cast_ite, Nat.cast_zero, hmon]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    if (d 0, d 1) ∈ Finset.antidiagonal n then ↑(n.choose (d 0)) else 0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    if (d 0, d 1) ∈ Finset.antidiagonal n then ↑(n.choose (d 0)) else 0
Tactic:
split_ifs with hd
Proof state after:
case pos
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∈ Finset.antidiagonal n
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    ↑(n.choose (d 0))

case neg
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
hmon :
  ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
hd : (d 0, d 1) ∉ Finset.antidiagonal n
⊢ ∑ x ∈ Finset.antidiagonal n,
      n.choose x.1 • MvPolynomial.coeff d ((MvPolynomial.monomial (Finsupp.single 0 x.1 + Finsupp.single 1 x.2)) 1) =
    0
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n : ℕ
⊢ ∀ (u v : ℕ),
    MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
Tactic:
intro u v
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v = (MvPolynomial.monomial (Finsupp.single 0 u + Finsupp.single 1 v)) 1
Tactic:
rw [MvPolynomial.monomial_eq]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * (Finsupp.single 0 u + Finsupp.single 1 v).prod fun n e => MvPolynomial.X n ^ e
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * (Finsupp.single 0 u + Finsupp.single 1 v).prod fun n e => MvPolynomial.X n ^ e
Tactic:
rw [Finsupp.prod_of_support_subset _ (Finset.subset_univ _)]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * ∏ x : Fin 2, MvPolynomial.X x ^ (Finsupp.single 0 u + Finsupp.single 1 v) x

case h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ ∀ i ∈ Finset.univ, MvPolynomial.X i ^ 0 = 1
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.C 1 * ∏ x : Fin 2, MvPolynomial.X x ^ (Finsupp.single 0 u + Finsupp.single 1 v) x
Tactic:
simp only [map_one, Fin.prod_univ_two, Fin.isValue, one_mul]
Proof state after:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.X 0 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 0 *
      MvPolynomial.X 1 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 1
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ MvPolynomial.X 0 ^ u * MvPolynomial.X 1 ^ v =
    MvPolynomial.X 0 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 0 *
      MvPolynomial.X 1 ^ (Finsupp.single 0 u + Finsupp.single 1 v) 1
Tactic:
simp only [Fin.isValue, Finsupp.coe_add, Pi.add_apply,
  Finsupp.single_eq_same, ne_eq, one_ne_zero, not_false_eq_true,
  Finsupp.single_eq_of_ne, add_zero, zero_ne_one, zero_add]
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
case h
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
⊢ ∀ i ∈ Finset.univ, MvPolynomial.X i ^ 0 = 1
Tactic:
exact fun i _ ↦ by simp only [pow_zero]
Proof state after:
no goals
Theorem: PowerSeries.coeff_add_pow
Proof state before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
d : Fin 2 →₀ ℕ
n u v : ℕ
i : Fin 2
x✝ : i ∈ Finset.univ
⊢ MvPolynomial.X i ^ 0 = 1
Tactic:
simp only [pow_zero]
Proof state after:
no goals