Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
Proof state before:
case mk.mk.mk.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ) {a : A}, 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
H : a + b = a' + b'
c : A := a - a'
hc : c = a - a'
haa' : a = a' + c
hbb' : b' = b + c
hcI : c ∈ I
hcJ : c ∈ J
Ha'c :
  ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Hbc :
  ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c) =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
s : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (a + 1)
hs_def : s = (range (n + 1)).sigma fun a => range (a + 1)
i : (x : (_ : ℕ) × ℕ) → x ∈ s → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
hi_def :
  i = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
t : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (n - a + 1)
ht_def : t = (range (n + 1)).sigma fun a => range (n - a + 1)
j : (y : (_ : ℕ) × ℕ) → y ∈ t → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
hj_def :
  j = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
⊢ ∑ x ∈ s, hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ t, hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
Tactic:
rw [Finset.sum_bij' i j _ _ _ _]
Proof state after:
case mk.mk.mk.mk.mk.mk
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ) {a : A}, 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
H : a + b = a' + b'
c : A := a - a'
hc : c = a - a'
haa' : a = a' + c
hbb' : b' = b + c
hcI : c ∈ I
hcJ : c ∈ J
Ha'c :
  ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Hbc :
  ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c) =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
s : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (a + 1)
hs_def : s = (range (n + 1)).sigma fun a => range (a + 1)
i : (x : (_ : ℕ) × ℕ) → x ∈ s → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
hi_def :
  i = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
t : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (n - a + 1)
ht_def : t = (range (n + 1)).sigma fun a => range (n - a + 1)
j : (y : (_ : ℕ) × ℕ) → y ∈ t → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
hj_def :
  j = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
⊢ ∀ (a : (_ : ℕ) × ℕ) (ha : a ∈ s),
    hI.dpow a.snd a' * hJ.dpow (n - a.fst) b * hI.dpow (a.fst - a.snd) c =
      hI.dpow (i a ha).fst a' * hJ.dpow (i a ha).snd b * hJ.dpow (n - (i a ha).fst - (i a ha).snd) c

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ) {a : A}, 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
H : a + b = a' + b'
c : A := a - a'
hc : c = a - a'
haa' : a = a' + c
hbb' : b' = b + c
hcI : c ∈ I
hcJ : c ∈ J
Ha'c :
  ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Hbc :
  ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c) =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
s : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (a + 1)
hs_def : s = (range (n + 1)).sigma fun a => range (a + 1)
i : (x : (_ : ℕ) × ℕ) → x ∈ s → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
hi_def :
  i = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
t : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (n - a + 1)
ht_def : t = (range (n + 1)).sigma fun a => range (n - a + 1)
j : (y : (_ : ℕ) × ℕ) → y ∈ t → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
hj_def :
  j = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
⊢ ∀ (a : (_ : ℕ) × ℕ) (ha : a ∈ s), i a ha ∈ t

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ) {a : A}, 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
H : a + b = a' + b'
c : A := a - a'
hc : c = a - a'
haa' : a = a' + c
hbb' : b' = b + c
hcI : c ∈ I
hcJ : c ∈ J
Ha'c :
  ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Hbc :
  ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c) =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
s : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (a + 1)
hs_def : s = (range (n + 1)).sigma fun a => range (a + 1)
i : (x : (_ : ℕ) × ℕ) → x ∈ s → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
hi_def :
  i = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
t : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (n - a + 1)
ht_def : t = (range (n + 1)).sigma fun a => range (n - a + 1)
j : (y : (_ : ℕ) × ℕ) → y ∈ t → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
hj_def :
  j = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
⊢ ∀ (a : (_ : ℕ) × ℕ) (ha : a ∈ t), j a ha ∈ s

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ) {a : A}, 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
H : a + b = a' + b'
c : A := a - a'
hc : c = a - a'
haa' : a = a' + c
hbb' : b' = b + c
hcI : c ∈ I
hcJ : c ∈ J
Ha'c :
  ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Hbc :
  ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c) =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
s : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (a + 1)
hs_def : s = (range (n + 1)).sigma fun a => range (a + 1)
i : (x : (_ : ℕ) × ℕ) → x ∈ s → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
hi_def :
  i = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
t : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (n - a + 1)
ht_def : t = (range (n + 1)).sigma fun a => range (n - a + 1)
j : (y : (_ : ℕ) × ℕ) → y ∈ t → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
hj_def :
  j = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
⊢ ∀ (a : (_ : ℕ) × ℕ) (ha : a ∈ s), j (i a ha) ⋯ = a

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ) {a : A}, 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
H : a + b = a' + b'
c : A := a - a'
hc : c = a - a'
haa' : a = a' + c
hbb' : b' = b + c
hcI : c ∈ I
hcJ : c ∈ J
Ha'c :
  ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Hbc :
  ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c) =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
s : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (a + 1)
hs_def : s = (range (n + 1)).sigma fun a => range (a + 1)
i : (x : (_ : ℕ) × ℕ) → x ∈ s → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
hi_def :
  i = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨m, n - k⟩
t : Finset ((_ : ℕ) × ℕ) := (range (n + 1)).sigma fun a => range (n - a + 1)
ht_def : t = (range (n + 1)).sigma fun a => range (n - a + 1)
j : (y : (_ : ℕ) × ℕ) → y ∈ t → (_ : ℕ) × ℕ :=
  fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
hj_def :
  j = fun x x_1 =>
    match x, x_1 with
    | ⟨k, m⟩, x => ⟨n - m, k⟩
⊢ ∀ (a : (_ : ℕ) × ℕ) (ha : a ∈ t), i (j a ha) ⋯ = a