Theorem: DividedPowerAlgebra.dp_sum (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ dp R q (s.sum x) = ∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)
Tactic:
apply DividedPowers.dpow_sum_aux'
State after:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (x : M), dp R 0 x = 1

case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (n : ℕ) (x y : M),
    dp R n (x + y) =
      ∑ x_1 ∈ antidiagonal n,
        match x_1 with
        | (k, l) => dp R k x * dp R l y

case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ {n : ℕ}, n ≠ 0 → dp R n 0 = 0

State before:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (x : M), dp R 0 x = 1
Tactic:
intro x
State after:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
x : M
⊢ dp R 0 x = 1

State before:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
x : M
⊢ dp R 0 x = 1
Tactic:
rw [dp_zero]
State after:
no goals

State before:
case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (n : ℕ) (x y : M),
    dp R n (x + y) =
      ∑ x_1 ∈ antidiagonal n,
        match x_1 with
        | (k, l) => dp R k x * dp R l y
Tactic:
intro n x y
State after:
case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
n : ℕ
x y : M
⊢ dp R n (x + y) =
    ∑ x_1 ∈ antidiagonal n,
      match x_1 with
      | (k, l) => dp R k x * dp R l y

State before:
case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
n : ℕ
x y : M
⊢ dp R n (x + y) =
    ∑ x_1 ∈ antidiagonal n,
      match x_1 with
      | (k, l) => dp R k x * dp R l y
Tactic:
rw [dp_add]
State after:
no goals

State before:
case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ {n : ℕ}, n ≠ 0 → dp R n 0 = 0
Tactic:
intro n hn
State after:
case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
n : ℕ
hn : n ≠ 0
⊢ dp R n 0 = 0

State before:
case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
n : ℕ
hn : n ≠ 0
⊢ dp R n 0 = 0
Tactic:
rw [dp_null R n, if_neg hn]
State after:
no goals