internlm/Lean-Github huggingface dataset:
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
⊢ ∑ x ∈ (range (n + 1)).sigma fun k => range (k + 1),
      hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) 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:
rw [Finset.sum_sigma']
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
⊢ ∑ x ∈ (range (n + 1)).sigma fun k => range (k + 1),
      hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ (range (n + 1)).sigma fun k => range (n - k + 1),
      hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
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
⊢ ∑ x ∈ (range (n + 1)).sigma fun k => range (k + 1),
      hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ (range (n + 1)).sigma fun k => range (n - k + 1),
      hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
Tactic:
set s := (Finset.range (n + 1)).sigma fun a : ℕ => Finset.range (a + 1) with hs_def
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)
⊢ ∑ x ∈ s, hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ (range (n + 1)).sigma fun k => range (n - k + 1),
      hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
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)
⊢ ∑ x ∈ s, hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ (range (n + 1)).sigma fun k => range (n - k + 1),
      hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
Tactic:
set i : ∀ x : Σ _ : ℕ, ℕ, x ∈ s → Σ _ : ℕ, ℕ := fun ⟨k, m⟩ _ => ⟨m, n - k⟩ with hi_def
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⟩
⊢ ∑ x ∈ s, hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ (range (n + 1)).sigma fun k => range (n - k + 1),
      hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
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⟩
⊢ ∑ x ∈ s, hI.dpow x.snd a' * hJ.dpow (n - x.fst) b * hI.dpow (x.fst - x.snd) c =
    ∑ x ∈ (range (n + 1)).sigma fun k => range (n - k + 1),
      hI.dpow x.fst a' * hJ.dpow x.snd b * hJ.dpow (n - x.fst - x.snd) c
Tactic:
set t := (Finset.range (n + 1)).sigma fun a : ℕ => Finset.range (n - a + 1) with ht_def
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)
⊢ ∑ 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
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)
⊢ ∑ 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:
set j : ∀ y : Σ _ : ℕ, ℕ, y ∈ t → Σ _ : ℕ, ℕ := fun ⟨k, m⟩ _ => ⟨n - m, k⟩ with hj_def
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⟩
⊢ ∑ 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
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'
⊢ a = a' + c
Tactic:
simp only [hc, add_sub_cancel]
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
⊢ b' = b + c
Tactic:
rw [← sub_eq_iff_eq_add'] 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
⊢ b' = b + 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
⊢ b' = b + 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
⊢ a + b - a' = b + 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
⊢ a + b - a' = b + c
Tactic:
rw [haa']
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
⊢ a' + c + b - a' = b + 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
⊢ a' + c + b - a' = b + 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
⊢ c ∈ J
Tactic:
rw [← sub_eq_iff_eq_add'.mpr hbb']
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
⊢ b' - b ∈ J
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
⊢ b' - b ∈ J
Tactic:
exact sub_mem hb' hb
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
⊢ ∑ 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
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
⊢ ∀ x ∈ range (n + 1),
    hI.dpow x (a' + c) * hJ.dpow (n - x) b = ∑ l ∈ range (x + 1), hI.dpow l a' * hJ.dpow (n - x) b * hI.dpow (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
⊢ ∀ x ∈ range (n + 1),
    hI.dpow x (a' + c) * hJ.dpow (n - x) b = ∑ l ∈ range (x + 1), hI.dpow l a' * hJ.dpow (n - x) b * hI.dpow (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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k (a' + c) * hJ.dpow (n - k) b = ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ hI.dpow k (a' + c) * hJ.dpow (n - k) b = ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
Tactic:
rw [hI.dpow_add' k ha' hcI]
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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a' * hI.dpow (k - k_1) c) * hJ.dpow (n - k) b =
    ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ (∑ k_1 ∈ range (k + 1), hI.dpow k_1 a' * hI.dpow (k - k_1) c) * hJ.dpow (n - k) b =
    ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c
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 : 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)
⊢ ∑ i ∈ range (k + 1), hI.dpow i a' * hI.dpow (k - i) c * hJ.dpow (n - k) b =
    ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∑ i ∈ range (k + 1), hI.dpow i a' * hI.dpow (k - i) c * hJ.dpow (n - k) b =
    ∑ l ∈ range (k + 1), hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∀ x ∈ range (k + 1),
    hI.dpow x a' * hI.dpow (k - x) c * hJ.dpow (n - k) b = hI.dpow x a' * hJ.dpow (n - k) b * hI.dpow (k - x) 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
k : ℕ
a✝ : k ∈ range (n + 1)
⊢ ∀ x ∈ range (k + 1),
    hI.dpow x a' * hI.dpow (k - x) c * hJ.dpow (n - k) b = hI.dpow x a' * hJ.dpow (n - k) b * hI.dpow (k - x) c
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 : 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