Theorem: DividedPowers.IdealAdd.dpow_factorsThrough
Proof state before:
case 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 ≤ n ∧ m + k ≤ n
⊢ m ≤ n

case 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 ≤ n ∧ m ≤ n - k
⊢ k ≤ n
Tactic:
exact le_trans (Nat.le_add_right _ _) h.2
Proof state after:
case 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 ≤ n ∧ m ≤ n - k
⊢ k ≤ n