internlm/Lean-Github huggingface dataset:
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)
⊢ ∑ 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'
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)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ ∀ x ∈ range (n - k + 1),
    hI.dpow i a * hI.dpow (k - i) a' * (hJ.dpow x b * hJ.dpow (n - k - x) b') =
      hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow x b * hJ.dpow (n - k - x) 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)
⊢ ∀ x ∈ range (n - k + 1),
    hI.dpow i a * hI.dpow (k - i) a' * (hJ.dpow x b * hJ.dpow (n - k - x) b') =
      hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow x b * hJ.dpow (n - k - x) b'
Tactic:
intro l _
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)
l : ℕ
a✝ : l ∈ range (n - k + 1)
⊢ hI.dpow i a * hI.dpow (k - i) a' * (hJ.dpow l b * hJ.dpow (n - k - l) b') =
    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)
l : ℕ
a✝ : l ∈ range (n - k + 1)
⊢ hI.dpow i a * hI.dpow (k - i) a' * (hJ.dpow l b * hJ.dpow (n - k - l) b') =
    hI.dpow i a * hI.dpow (k - i) a' * hJ.dpow l b * hJ.dpow (n - k - l) b'
Tactic:
ring
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'
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),
    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'
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'
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 : ℕ
a✝ : 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'
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'
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 : ℕ
a✝ : 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'
Tactic:
rw [dpow_eq hI hJ hIJ k ha 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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hJ.dpow (k - k_1) 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'
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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hJ.dpow (k - k_1) 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'
Tactic:
rw [dpow_eq hI hJ hIJ (n - k) ha' 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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hJ.dpow (k - k_1) b) *
      ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) 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'
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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a * hJ.dpow (k - k_1) b) *
      ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) 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'
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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (k + 1),
      hI.dpow i a * hJ.dpow (k - i) b * ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) 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'
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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (k + 1),
      hI.dpow i a * hJ.dpow (k - i) b * ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) 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'
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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∀ x ∈ range (k + 1),
    hI.dpow x a * hJ.dpow (k - x) b * ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) b' =
      ∑ l ∈ range (n - k + 1), hI.dpow x a * hI.dpow l a' * hJ.dpow (k - x) 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'
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 : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∀ x ∈ range (k + 1),
    hI.dpow x a * hJ.dpow (k - x) b * ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) b' =
      ∑ l ∈ range (n - k + 1), hI.dpow x a * hI.dpow l a' * hJ.dpow (k - x) 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'
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 : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ hI.dpow i a * hJ.dpow (k - i) b * ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) b' =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) 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'
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 : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ hI.dpow i a * hJ.dpow (k - i) b * ∑ k_1 ∈ range (n - k + 1), hI.dpow k_1 a' * hJ.dpow (n - k - k_1) b' =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) 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'
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 : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ ∑ i_1 ∈ range (n - k + 1), hI.dpow i a * hJ.dpow (k - i) b * (hI.dpow i_1 a' * hJ.dpow (n - k - i_1) b') =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) 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'
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 : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ ∑ i_1 ∈ range (n - k + 1), hI.dpow i a * hJ.dpow (k - i) b * (hI.dpow i_1 a' * hJ.dpow (n - k - i_1) b') =
    ∑ l ∈ range (n - k + 1), hI.dpow i a * hI.dpow l a' * hJ.dpow (k - i) 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'
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 : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ ∀ x ∈ range (n - k + 1),
    hI.dpow i a * hJ.dpow (k - i) b * (hI.dpow x a' * hJ.dpow (n - k - x) b') =
      hI.dpow i a * hI.dpow x a' * hJ.dpow (k - i) b * hJ.dpow (n - k - x) 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'
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 : ℕ
a✝¹ : k ∈ range (n + 1)
i : ℕ
a✝ : i ∈ range (k + 1)
⊢ ∀ x ∈ range (n - k + 1),
    hI.dpow i a * hJ.dpow (k - i) b * (hI.dpow x a' * hJ.dpow (n - k - x) b') =
      hI.dpow i a * hI.dpow x a' * hJ.dpow (k - i) b * hJ.dpow (n - k - x) b'
Tactic:
intro j _
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'
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 : ℕ
a✝² : k ∈ range (n + 1)
i : ℕ
a✝¹ : i ∈ range (k + 1)
j : ℕ
a✝ : j ∈ range (n - k + 1)
⊢ hI.dpow i a * hJ.dpow (k - i) b * (hI.dpow j a' * hJ.dpow (n - k - j) b') =
    hI.dpow i a * hI.dpow j a' * hJ.dpow (k - i) b * hJ.dpow (n - k - j) 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'
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 : ℕ
a✝² : k ∈ range (n + 1)
i : ℕ
a✝¹ : i ∈ range (k + 1)
j : ℕ
a✝ : j ∈ range (n - k + 1)
⊢ hI.dpow i a * hJ.dpow (k - i) b * (hI.dpow j a' * hJ.dpow (n - k - j) b') =
    hI.dpow i a * hI.dpow j a' * hJ.dpow (k - i) b * hJ.dpow (n - k - j) b'
Tactic:
ring
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 : ℕ) {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]
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 : ℕ) {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
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 : ℕ) {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
Proof state after:
no goals