Theorem: DividedPowers.IdealAdd.dpow_eq (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 : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [IdealAdd.dpow]
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 : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Function.extend
      (fun x =>
        match x with
        | (a, b) => ↑a + ↑b)
      (fun x =>
        match x with
        | (a, b) => ∑ k ∈ range (n + 1), hI.dpow k ↑a * hJ.dpow (n - k) ↑b)
      (Function.const A 0) (a + b) =
    ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b

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 : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Function.extend
      (fun x =>
        match x with
        | (a, b) => ↑a + ↑b)
      (fun x =>
        match x with
        | (a, b) => ∑ k ∈ range (n + 1), hI.dpow k ↑a * hJ.dpow (n - k) ↑b)
      (Function.const A 0) (a + b) =
    ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [(dpow_factorsThrough hI hJ hIJ n).extend_apply _ (⟨⟨a, ha⟩, ⟨b, hb⟩⟩ : I × J)]
State after:
no goals