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
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
Tactic:
rintro ⟨k, m⟩ h
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, m⟩ ∈ s
⊢ j (i ⟨k, m⟩ h) ⋯ = ⟨k, m⟩
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, m⟩ ∈ s
⊢ j (i ⟨k, m⟩ h) ⋯ = ⟨k, m⟩
Tactic:
simp only [hs_def, mem_sigma, mem_range, Nat.lt_succ_iff] at h
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, m⟩ ∈ s
h : k ≤ n ∧ m ≤ k
⊢ j (i ⟨k, m⟩ h✝) ⋯ = ⟨k, m⟩
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, m⟩ ∈ s
h : k ≤ n ∧ m ≤ k
⊢ j (i ⟨k, m⟩ h✝) ⋯ = ⟨k, m⟩
Tactic:
simp only [hj_def, Sigma.mk.inj_iff, heq_eq_eq, and_true]
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, m⟩ ∈ s
h : k ≤ n ∧ m ≤ k
⊢ n - (n - k) = k
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, m⟩ ∈ s
h : k ≤ n ∧ m ≤ k
⊢ n - (n - k) = k
Tactic:
exact Nat.sub_sub_self 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⟩
⊢ ∀ (a : (_ : ℕ) × ℕ) (ha : a ∈ t), i (j a ha) ⋯ = a
Tactic:
rintro ⟨u, v⟩ h
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⟩
u v : ℕ
h : ⟨u, v⟩ ∈ t
⊢ i (j ⟨u, v⟩ h) ⋯ = ⟨u, v⟩
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⟩
u v : ℕ
h : ⟨u, v⟩ ∈ t
⊢ i (j ⟨u, v⟩ h) ⋯ = ⟨u, v⟩
Tactic:
simp only [ht_def, mem_sigma, mem_range, Nat.lt_succ_iff] at h
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⟩
u v : ℕ
h✝ : ⟨u, v⟩ ∈ t
h : u ≤ n ∧ v ≤ n - u
⊢ i (j ⟨u, v⟩ h✝) ⋯ = ⟨u, v⟩
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⟩
u v : ℕ
h✝ : ⟨u, v⟩ ∈ t
h : u ≤ n ∧ v ≤ n - u
⊢ i (j ⟨u, v⟩ h✝) ⋯ = ⟨u, v⟩
Tactic:
simp only [hi_def, Sigma.mk.inj_iff, heq_eq_eq, true_and]
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⟩
u v : ℕ
h✝ : ⟨u, v⟩ ∈ t
h : u ≤ n ∧ v ≤ n - u
⊢ n - (n - v) = v
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⟩
u v : ℕ
h✝ : ⟨u, v⟩ ∈ t
h : u ≤ n ∧ v ≤ n - u
⊢ n - (n - v) = v
Tactic:
exact Nat.sub_sub_self (le_trans h.2 (Nat.sub_le n u))
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [IdealAdd.dpow]
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Function.extend
      (fun x =>
        match x with
        | (a, b) => ↑a + ↑b)
      (fun x =>
        match x with
        | (a, b) => ∑ k ∈ range (n + 1), hI.dpow k ↑a * hJ.dpow (n - k) ↑b)
      (Function.const A 0) (a + b) =
    ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Theorem: DividedPowers.IdealAdd.dpow_eq
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Function.extend
      (fun x =>
        match x with
        | (a, b) => ↑a + ↑b)
      (fun x =>
        match x with
        | (a, b) => ∑ k ∈ range (n + 1), hI.dpow k ↑a * hJ.dpow (n - k) ↑b)
      (Function.const A 0) (a + b) =
    ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b
Tactic:
rw [(dpow_factorsThrough hI hJ hIJ n).extend_apply _ (⟨⟨a, ha⟩, ⟨b, hb⟩⟩ : I × J)]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x : A
hx : x ∈ I
⊢ dpow hI hJ n x = hI.dpow n x
Tactic:
rw [← add_zero x]
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x : A
hx : x ∈ I
⊢ dpow hI hJ n (x + 0) = hI.dpow n (x + 0)
Theorem: DividedPowers.IdealAdd.dpow_eq_of_mem_left
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x : A
hx : x ∈ I
⊢ dpow hI hJ n (x + 0) = hI.dpow n (x + 0)
Tactic:
rw [dpow_eq hI hJ hIJ n hx J.zero_mem]
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
n : ℕ
x : A
hx : x ∈ I
⊢ ∑ k ∈ range (n + 1), hI.dpow k x * hJ.dpow (n - k) 0 = hI.dpow n (x + 0)