Theorem: DividedPowers.IdealAdd.dpow_add (DividedPowers/IdealAdd.lean)

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J →
      y ∈ I + J →
        dpow hI hJ n (x + y) =
          ∑ x_3 ∈ antidiagonal n,
            match x_3 with
            | (k, l) => dpow hI hJ k x * dpow hI hJ l y
Tactic:
simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ x_3 ∈ range n.succ, dpow hI hJ x_3 x * dpow hI hJ (n - x_3) y

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ x_3 ∈ range n.succ, dpow hI hJ x_3 x * dpow hI hJ (n - x_3) y
Tactic:
exact dpow_add' hI hJ hIJ
State after:
no goals