internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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
k : ℕ
a✝¹ : k ∈ range (n + 1)
l : ℕ
a✝ : l ∈ range (k + 1)
⊢ hI.dpow l a' * hI.dpow (k - l) c * hJ.dpow (n - k) b = hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Tactic:
ring
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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
⊢ ∑ 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
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 : 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
⊢ ∀ x ∈ range (n + 1),
    hI.dpow x a' * hJ.dpow (n - x) (b + c) = ∑ l ∈ range (n - x + 1), hI.dpow x a' * hJ.dpow l b * hJ.dpow (n - x - l) c
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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
⊢ ∀ x ∈ range (n + 1),
    hI.dpow x a' * hJ.dpow (n - x) (b + c) = ∑ l ∈ range (n - x + 1), hI.dpow x a' * hJ.dpow l b * hJ.dpow (n - x - l) c
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 : 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k a' * hJ.dpow (n - k) (b + c) = ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k a' * hJ.dpow (n - k) (b + c) = ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
Tactic:
rw [hJ.dpow_add' (n - k) hb hcJ]
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 : 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) c =
    ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k a' * ∑ k_1 ∈ range (n - k + 1), hJ.dpow k_1 b * hJ.dpow (n - k - k_1) c =
    ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
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 : 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (n - k + 1), hI.dpow k a' * (hJ.dpow i b * hJ.dpow (n - k - i) c) =
    ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (n - k + 1), hI.dpow k a' * (hJ.dpow i b * hJ.dpow (n - k - i) c) =
    ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c
Tactic:
ring_nf
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
Proof state before:
case mk.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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ hI.dpow m a' * hJ.dpow (n - k) b * hI.dpow (k - m) c = hI.dpow m a' * hJ.dpow (n - k) b * hJ.dpow (n - m - (n - k)) c
Tactic:
apply congr_arg₂ _ rfl
Proof state after:
case mk.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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ hI.dpow (k - m) c = hJ.dpow (n - m - (n - k)) c
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
Proof state before:
case mk.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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ hI.dpow (k - m) c = hJ.dpow (n - m - (n - k)) c
Tactic:
suffices h : n - m - (n - k) = k - m by
  rw [h]
  exact hIJ _ ⟨hcI, hcJ⟩
Proof state after:
case mk.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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ n - m - (n - k) = k - m
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
Proof state before:
case mk.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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ n - m - (n - k) = k - m
Tactic:
rw [Nat.sub_sub, add_comm, ← Nat.sub_sub, Nat.sub_sub_self ?_]
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 : 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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ k ≤ n
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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⟩
k m : ℕ
h : ⟨k, m⟩ ∈ s
⊢ k ≤ n
Tactic:
simp only [hs_def, mem_sigma, mem_range] at h
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 : 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⟩
k m : ℕ
h : k < n + 1 ∧ m < k + 1
⊢ k ≤ n
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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⟩
k m : ℕ
h : k < n + 1 ∧ m < k + 1
⊢ k ≤ n
Tactic:
exact Nat.le_of_lt_succ h.1
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
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 : 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⟩
k m : ℕ
h✝ : ⟨k, m⟩ ∈ s
h : n - m - (n - k) = k - m
⊢ hI.dpow (k - m) c = hJ.dpow (n - m - (n - k)) c
Tactic:
rw [h]
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 : 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⟩
k m : ℕ
h✝ : ⟨k, m⟩ ∈ s
h : n - m - (n - k) = k - m
⊢ hI.dpow (k - m) c = hJ.dpow (k - m) c