internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_mul
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b =
    (∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), ↑(u.choose x.1.1) * ↑(v.choose x.1.2)) *
        hI.dpow u a *
      hJ.dpow v b
Tactic:
simp only [Finset.sum_mul]
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b =
    ∑ i ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑(u.choose i.1.1) * ↑(v.choose i.1.2) * hI.dpow u a * hJ.dpow v b
Theorem: DividedPowers.IdealAdd.dpow_mul
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∑ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b =
    ∑ i ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
      ↑(u.choose i.1.1) * ↑(v.choose i.1.2) * hI.dpow u a * hJ.dpow v b
Tactic:
apply Finset.sum_congr rfl
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∀ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
    ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b =
      ↑(u.choose x.1.1) * ↑(v.choose x.1.2) * hI.dpow u a * hJ.dpow v b
Theorem: DividedPowers.IdealAdd.dpow_mul
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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
⊢ ∀ x ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
    ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b =
      ↑(u.choose x.1.1) * ↑(v.choose x.1.2) * hI.dpow u a * hJ.dpow v b
Tactic:
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ hx
Proof state after:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((((i, j), k, l).1.1 + ((i, j), k, l).2.1).choose ((i, j), k, l).1.1) *
          ↑((((i, j), k, l).1.2 + ((i, j), k, l).2.2).choose ((i, j), k, l).1.2) *
        hI.dpow (((i, j), k, l).1.1 + ((i, j), k, l).2.1) a *
      hJ.dpow (((i, j), k, l).1.2 + ((i, j), k, l).2.2) b =
    ↑(u.choose ((i, j), k, l).1.1) * ↑(v.choose ((i, j), k, l).1.2) * hI.dpow u a * hJ.dpow v b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((((i, j), k, l).1.1 + ((i, j), k, l).2.1).choose ((i, j), k, l).1.1) *
          ↑((((i, j), k, l).1.2 + ((i, j), k, l).2.2).choose ((i, j), k, l).1.2) *
        hI.dpow (((i, j), k, l).1.1 + ((i, j), k, l).2.1) a *
      hJ.dpow (((i, j), k, l).1.2 + ((i, j), k, l).2.2) b =
    ↑(u.choose ((i, j), k, l).1.1) * ↑(v.choose ((i, j), k, l).1.2) * hI.dpow u a * hJ.dpow v b
Tactic:
simp only
Proof state after:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : ((i, j), k, l) ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n)
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Tactic:
simp only [hs_def, mem_product, mem_antidiagonal, and_imp, Prod.forall, mem_filter,
  Prod.mk.injEq] at hx
Proof state after:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Tactic:
rw [hx.2.1]
Proof state after:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑(u.choose i) * ↑((j + l).choose j) * hI.dpow u a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
u v : ℕ
a✝ : (u, v) ∈ antidiagonal (m + n)
i j k l : ℕ
hx : (i + j = m ∧ k + l = n) ∧ i + k = u ∧ j + l = v
⊢ ↑(u.choose i) * ↑((j + l).choose j) * hI.dpow u a * hJ.dpow (j + l) b =
    ↑(u.choose i) * ↑(v.choose j) * hI.dpow u a * hJ.dpow v b
Tactic:
rw [hx.2.2]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case h
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ ∑ x ∈ antidiagonal m, u.choose x.1 * v.choose x.2 = (m + n).choose m
Tactic:
rw [← Nat.add_choose_eq]
Proof state after:
case h
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ (u + v).choose m = (m + n).choose m
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case h
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ (u + v).choose m = (m + n).choose m
Tactic:
rw [h]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_mul
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h : u + v = m + n
⊢ ∀ (x : ℕ × ℕ), u < x.1 ∨ v < x.2 → (fun x => u.choose x.1 * v.choose x.2) x = 0
Tactic:
intro x 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 ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h✝ : u + v = m + n
x : ℕ × ℕ
h : u < x.1 ∨ v < x.2
⊢ (fun x => u.choose x.1 * v.choose x.2) x = 0
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case inr
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
m n : ℕ
a : A
ha : a ∈ I
b : A
hb : b ∈ J
hf :
  ∀ (x : (ℕ × ℕ) × ℕ × ℕ),
    hI.dpow x.1.1 a * hJ.dpow x.1.2 b * (hI.dpow x.2.1 a * hJ.dpow x.2.2 b) =
      ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
        hJ.dpow (x.1.2 + x.2.2) b
s : (ℕ × ℕ) × ℕ × ℕ → ℕ × ℕ := fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs_def : s = fun x => (x.1.1 + x.2.1, x.1.2 + x.2.2)
hs : ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
hs' :
  ∑ y ∈ antidiagonal (m + n),
      ∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
        ↑((x.1.1 + x.2.1).choose x.1.1) * ↑((x.1.2 + x.2.2).choose x.1.2) * hI.dpow (x.1.1 + x.2.1) a *
          hJ.dpow (x.1.2 + x.2.2) b =
    ∑ y ∈ antidiagonal (m + n),
      ↑(∑ x ∈ filter (fun x => (fun x => s x) x = y) (antidiagonal m ×ˢ antidiagonal n),
              y.1.choose x.1.1 * y.2.choose x.1.2) *
          hI.dpow y.1 a *
        hJ.dpow y.2 b
u v : ℕ
h✝ : u + v = m + n
x : ℕ × ℕ
h : v < x.2
⊢ (fun x => u.choose x.1 * v.choose x.2) x = 0
Tactic:
simp only [Nat.choose_eq_zero_of_lt h, MulZeroClass.zero_mul, MulZeroClass.mul_zero]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_mem
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
hn : n ≠ 0
hx : x ∈ I + J
⊢ dpow hI hJ n x ∈ I + J
Tactic:
rw [Ideal.add_eq_sup, Submodule.mem_sup] at hx
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
hn : n ≠ 0
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ n x ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_mem
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
hn : n ≠ 0
hx : ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ dpow hI hJ n x ∈ I + J
Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx
Proof state after:
case intro.intro.intro.intro
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (a + b) ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case intro.intro.intro.intro
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ n (a + b) ∈ I + J
Tactic:
rw [dpow_eq hI hJ hIJ _ ha hb]
Proof state after:
case intro.intro.intro.intro
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_mem
Proof state before:
case intro.intro.intro.intro
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ range (n + 1), hI.dpow k a * hJ.dpow (n - k) b ∈ I + J
Tactic:
apply Submodule.sum_mem (I ⊔ J)
Proof state after:
case intro.intro.intro.intro
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ c ∈ range (n + 1), hI.dpow c a * hJ.dpow (n - c) b ∈ I ⊔ J