Theorem: DividedPowers.dpow_sum (DividedPowers/Basic.lean)

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
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

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
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

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
State after:
no goals

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
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

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)]
State after:
no goals

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
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

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
State after:
no goals