internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro
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 : ℕ
y a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ y ∈ I ⊔ J → dpow hI hJ n (a + b + y) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) y
Tactic:
rw [Submodule.mem_sup]
Proof state after:
case intro.intro.intro.intro
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 : ℕ
y a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∃ y_1 ∈ I, ∃ z ∈ J, y_1 + z = y) →
    dpow hI hJ n (a + b + y) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) y
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro
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 : ℕ
y a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ (∃ y_1 ∈ I, ∃ z ∈ J, y_1 + z = y) →
    dpow hI hJ n (a + b + y) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) y
Tactic:
rintro ⟨a', ha', b', hb', rfl⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
⊢ dpow hI hJ n (a + b + (a' + b')) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
⊢ dpow hI hJ n (a + b + (a' + b')) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
rw [add_add_add_comm a b a' b']
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
⊢ dpow hI hJ n (a + a' + (b + b')) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
⊢ dpow hI hJ n (a + a' + (b + b')) = ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
rw [dpow_eq hI hJ hIJ n (Submodule.add_mem I ha ha') (Submodule.add_mem J hb hb')]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
let f : ℕ × ℕ × ℕ × ℕ → A := fun ⟨i, j, k, l⟩ =>
  hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
have hf1 :
  ∀ k ∈ Finset.range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      (Finset.range (k + 1)).sum fun i =>
        (Finset.range (n - k + 1)).sum fun l =>
          hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b' := by
  intro k _
  rw [hI.dpow_add' k ha ha']; rw [hJ.dpow_add' (n - k) hb hb']
  rw [Finset.sum_mul]
  apply Finset.sum_congr rfl
  intro i _
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro l _
  ring
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
rw [Finset.sum_congr rfl hf1]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow (x - i) a' * hJ.dpow l b * hJ.dpow (n - x - l) b' =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow (x - i) a' * hJ.dpow l b * hJ.dpow (n - x - l) b' =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
have hf2 :
  ∀ k ∈ Finset.range (n + 1),
    dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b') =
      (Finset.range (k + 1)).sum fun i =>
        (Finset.range (n - k + 1)).sum fun l =>
          hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) b * hJ.dpow (n - k - l) b' :=
  by
  intro k _
  rw [dpow_eq hI hJ hIJ k ha hb]
  rw [dpow_eq hI hJ hIJ (n - k) ha' hb']
  rw [Finset.sum_mul]
  apply Finset.sum_congr rfl
  intro i _
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro j _
  ring
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
hf2 :
  ∀ k ∈ range (n + 1),
    dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) b * hJ.dpow (n - k - l) b'
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow (x - i) a' * hJ.dpow l b * hJ.dpow (n - x - l) b' =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
hf2 :
  ∀ k ∈ range (n + 1),
    dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) b * hJ.dpow (n - k - l) b'
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow (x - i) a' * hJ.dpow l b * hJ.dpow (n - x - l) b' =
    ∑ k ∈ range (n + 1), dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b')
Tactic:
rw [Finset.sum_congr rfl hf2]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
hf2 :
  ∀ k ∈ range (n + 1),
    dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) b * hJ.dpow (n - k - l) b'
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow (x - i) a' * hJ.dpow l b * hJ.dpow (n - x - l) b' =
    ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (x - i) b * hJ.dpow (n - x - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
hf1 :
  ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
hf2 :
  ∀ k ∈ range (n + 1),
    dpow hI hJ k (a + b) * dpow hI hJ (n - k) (a' + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) b * hJ.dpow (n - k - l) b'
⊢ ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow (x - i) a' * hJ.dpow l b * hJ.dpow (n - x - l) b' =
    ∑ x ∈ range (n + 1),
      ∑ i ∈ range (x + 1),
        ∑ l ∈ range (n - x + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (x - i) b * hJ.dpow (n - x - l) b'
Tactic:
convert Finset.sum_4_rw f n
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
⊢ ∀ k ∈ range (n + 1),
    hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
      ∑ i ∈ range (k + 1),
        ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
intro k _
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k (a + a') * hJ.dpow (n - k) (b + b') =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
rw [hI.dpow_add' k ha ha']
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hI.dpow (k - k_1) a') * hJ.dpow (n - k) (b + b') =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hI.dpow (k - k_1) a') * hJ.dpow (n - k) (b + b') =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
rw [hJ.dpow_add' (n - k) hb hb']
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hI.dpow (k - k_1) a') *
      ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hI.dpow (k - k_1) a') *
      ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
rw [Finset.sum_mul]
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (k + 1),
      hI.dpow i a * hI.dpow (k - i) a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (k + 1),
      hI.dpow i a * hI.dpow (k - i) a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
    ∑ i ∈ range (k + 1),
      ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
apply Finset.sum_congr rfl
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∀ x ∈ range (k + 1),
    hI.dpow x a * hI.dpow (k - x) a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
      ∑ l ∈ range (n - k + 1), hI.dpow x a * hI.dpow (k - x) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∀ x ∈ range (k + 1),
    hI.dpow x a * hI.dpow (k - x) a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
      ∑ l ∈ range (n - k + 1), hI.dpow x a * hI.dpow (k - x) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
intro i _
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ hI.dpow i a * hI.dpow (k - i) a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Theorem: DividedPowers.IdealAdd.dpow_add'
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ hI.dpow i a * hI.dpow (k - i) a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) b' =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
rw [Finset.mul_sum]
Proof 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
a' : A
ha' : a' ∈ I
b' : A
hb' : b' ∈ J
f : ℕ × ℕ × ℕ × ℕ → A :=
  fun x =>
    match x with
    | (i, j, k, l) => hI.dpow i a * hI.dpow j a' * hJ.dpow k b * hJ.dpow l b'
k : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ ∑ i_1 ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * (hJ.dpow i_1 b * hJ.dpow (n - k - i_1) b') =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'