internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (homogeneousComponent w i) f d) (f d)
Tactic:
have hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0 := by
  intro p h
  rw [← coeff_apply (homogeneousComponent w p f) d, coeff_homogeneousComponent,
    if_neg (Ne.symm h)]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ HasSum (fun i => (homogeneousComponent w i) f d) (f d)
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ HasSum (fun i => (homogeneousComponent w i) f d) (f d)
Tactic:
convert hasSum_single (weight w d) hd using 1
Proof state after:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ f d = (homogeneousComponent w ((weight w) d)) f d
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
Tactic:
intro p h
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : p ≠ (weight w) d
⊢ (homogeneousComponent w p) f d = 0
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : p ≠ (weight w) d
⊢ (homogeneousComponent w p) f d = 0
Tactic:
rw [← coeff_apply (homogeneousComponent w p f) d, coeff_homogeneousComponent,
  if_neg (Ne.symm h)]
Proof state after:
no goals
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ f d = (homogeneousComponent w ((weight w) d)) f d
Tactic:
rw [← coeff_apply f d, ← coeff_apply (homogeneousComponent w (weight w d) f) d,
  coeff_homogeneousComponent]
Proof state after:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ (coeff α d) f = if (weight w) d = (weight w) d then (coeff α d) f else 0
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (b' : ℕ), b' ≠ (weight w) d → (homogeneousComponent w b') f d = 0
⊢ (coeff α d) f = if (weight w) d = (weight w) d then (coeff α d) f else 0
Tactic:
simp only [eq_self_iff_true, if_true]
Proof state after:
no goals
Theorem: MvPowerSeries.as_tsum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = ∑' (p : ℕ), (homogeneousComponent w p) f
Tactic:
haveI := t2Space σ α
Proof state after:
σ : Type u_2
α : Type u_1
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
w : σ → ℕ
f : MvPowerSeries σ α
this : T2Space (MvPowerSeries σ α)
⊢ f = ∑' (p : ℕ), (homogeneousComponent w p) f
Theorem: MvPowerSeries.as_tsum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
w : σ → ℕ
f : MvPowerSeries σ α
this : T2Space (MvPowerSeries σ α)
⊢ f = ∑' (p : ℕ), (homogeneousComponent w p) f
Tactic:
exact HasSum.unique (hasSum_of_homogeneous_components_self w f)
 (homogeneous_components_self_summable w f).hasSum
Proof state after:
no goals
Theorem: Polynomial.C_eq_smul_one
Proof state before:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ C a = a • 1
Tactic:
rw [← C_mul', mul_one]
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 : ℕ
⊢ Function.FactorsThrough
    (fun x =>
      match x with
      | (a, b) => ∑ k ∈ range (n + 1), hI.dpow k ↑a * hJ.dpow (n - k) ↑b)
    fun x =>
    match x with
    | (a, b) => ↑a + ↑b
Tactic:
dsimp [Function.FactorsThrough]
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 b : ↥I × ↥J⦄,
    ↑a.1 + ↑a.2 = ↑b.1 + ↑b.2 →
      ∑ k ∈ range (n + 1), hI.dpow k ↑a.1 * hJ.dpow (n - k) ↑a.2 =
        ∑ k ∈ range (n + 1), hI.dpow k ↑b.1 * hJ.dpow (n - k) ↑b.2
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 b : ↥I × ↥J⦄,
    ↑a.1 + ↑a.2 = ↑b.1 + ↑b.2 →
      ∑ k ∈ range (n + 1), hI.dpow k ↑a.1 * hJ.dpow (n - k) ↑a.2 =
        ∑ k ∈ range (n + 1), hI.dpow k ↑b.1 * hJ.dpow (n - k) ↑b.2
Tactic:
rintro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ⟨⟨a', ha'⟩, ⟨b', hb'⟩⟩ H
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, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = ↑(⟨a', ha'⟩, ⟨b', hb'⟩).1 + ↑(⟨a', ha'⟩, ⟨b', hb'⟩).2
⊢ ∑ k ∈ range (n + 1), hI.dpow k ↑(⟨a, ha⟩, ⟨b, hb⟩).1 * hJ.dpow (n - k) ↑(⟨a, ha⟩, ⟨b, hb⟩).2 =
    ∑ k ∈ range (n + 1), hI.dpow k ↑(⟨a', ha'⟩, ⟨b', hb'⟩).1 * hJ.dpow (n - k) ↑(⟨a', ha'⟩, ⟨b', hb'⟩).2
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, ha⟩, ⟨b, hb⟩).1 + ↑(⟨a, ha⟩, ⟨b, hb⟩).2 = ↑(⟨a', ha'⟩, ⟨b', hb'⟩).1 + ↑(⟨a', ha'⟩, ⟨b', hb'⟩).2
⊢ ∑ k ∈ range (n + 1), hI.dpow k ↑(⟨a, ha⟩, ⟨b, hb⟩).1 * hJ.dpow (n - k) ↑(⟨a, ha⟩, ⟨b, hb⟩).2 =
    ∑ k ∈ range (n + 1), hI.dpow k ↑(⟨a', ha'⟩, ⟨b', hb'⟩).1 * hJ.dpow (n - k) ↑(⟨a', ha'⟩, ⟨b', hb'⟩).2
Tactic:
dsimp only at H ⊢
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'
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
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'
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
Tactic:
set c := a - a' with hc
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'
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
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'
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
Tactic:
have haa' : a = a' + c := by simp only [hc, add_sub_cancel]
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
Tactic:
have hbb' : b' = b + c := by
  rw [← sub_eq_iff_eq_add'] at H ; rw [← H]; rw [haa']; ring
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
Tactic:
have hcI : c ∈ I := sub_mem ha ha'
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
Tactic:
have hcJ : c ∈ J := by
  rw [← sub_eq_iff_eq_add'.mpr hbb']; exact sub_mem hb' hb
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b = ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) b'
Tactic:
rw [haa', hbb']
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + 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
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c)
Tactic:
have Ha'c : ((Finset.range (n + 1)).sum
  fun k : ℕ => hI.dpow k (a' + c) * hJ.dpow (n - k) b) =
    (Finset.range (n + 1)).sum
      fun k : ℕ => (Finset.range (k + 1)).sum fun l : ℕ =>
        hI.dpow l a' * hJ.dpow (n - k) b * hI.dpow (k - l) c := by
  apply Finset.sum_congr rfl
  intro k _
  rw [hI.dpow_add' k ha' hcI]
  rw [Finset.sum_mul]
  apply Finset.sum_congr rfl
  intro l _
  ring
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
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + 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
⊢ ∑ k ∈ range (n + 1), hI.dpow k (a' + c) * hJ.dpow (n - k) b =
    ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c)
Tactic:
rw [Ha'c]
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
⊢ ∑ 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)
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
⊢ ∑ 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)
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
⊢ ∑ 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), hI.dpow k a' * hJ.dpow (n - k) (b + 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
⊢ ∑ 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), hI.dpow k a' * hJ.dpow (n - k) (b + c)
Tactic:
have Hbc : ((Finset.range (n + 1)).sum
  fun k : ℕ => hI.dpow k a' * hJ.dpow (n - k) (b + c)) =
    (Finset.range (n + 1)).sum
      fun k : ℕ => (Finset.range (n - k + 1)).sum
        fun l : ℕ => hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c := by
  apply Finset.sum_congr rfl
  intro k _
  rw [hJ.dpow_add' (n - k) hb hcJ]
  rw [Finset.mul_sum]; ring_nf
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 =
    ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + 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 =
    ∑ k ∈ range (n + 1), hI.dpow k a' * hJ.dpow (n - k) (b + c)
Tactic:
rw [Hbc]
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 =
    ∑ k ∈ range (n + 1), ∑ l ∈ range (n - k + 1), hI.dpow k a' * hJ.dpow l b * hJ.dpow (n - k - l) c