internlm/Lean-Github huggingface dataset:
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 ∈ filter (fun x => s x = (u, v)) (antidiagonal m ×ˢ antidiagonal n), u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m
Tactic:
simp only [hs_def, Prod.mk.injEq]
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
⊢ ∑ x ∈ filter (fun x => x.1.1 + x.2.1 = u ∧ x.1.2 + x.2.2 = v) (antidiagonal m ×ˢ antidiagonal n),
      u.choose x.1.1 * v.choose x.1.2 =
    (m + n).choose m
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
⊢ ∀ (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
Tactic:
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow ((i, j), k, l).1.1 a * hJ.dpow ((i, j), k, l).1.2 b *
      (hI.dpow ((i, j), k, l).2.1 a * hJ.dpow ((i, j), k, l).2.2 b) =
    ↑((((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
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow ((i, j), k, l).1.1 a * hJ.dpow ((i, j), k, l).1.2 b *
      (hI.dpow ((i, j), k, l).2.1 a * hJ.dpow ((i, j), k, l).2.2 b) =
    ↑((((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
Tactic:
dsimp
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * hJ.dpow j b * (hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * hJ.dpow j b * (hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [mul_assoc]
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * (hI.dpow k a * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * (hI.dpow k a * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [← mul_assoc (hJ.dpow j b) _ _]
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hJ.dpow j b * hI.dpow k a * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [mul_comm (hJ.dpow j b)]
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * hJ.dpow j b * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * hJ.dpow j b * hJ.dpow l b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [mul_assoc]
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (hJ.dpow j b * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (hJ.dpow j b * hJ.dpow l b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [hJ.dpow_mul j l hb]
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * (hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b)) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [← mul_assoc]
Proof state after:
case 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
i j k l : ℕ
⊢ hI.dpow i a * hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ hI.dpow i a * hI.dpow k a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
rw [hI.dpow_mul i k ha]
Proof state after:
case 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
i j k l : ℕ
⊢ ↑((i + k).choose i) * hI.dpow (i + k) a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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
i j k l : ℕ
⊢ ↑((i + k).choose i) * hI.dpow (i + k) a * (↑((j + l).choose j) * hJ.dpow (j + l) b) =
    ↑((i + k).choose i) * ↑((j + l).choose j) * hI.dpow (i + k) a * hJ.dpow (j + l) b
Tactic:
ring
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)
⊢ ∀ x ∈ antidiagonal m ×ˢ antidiagonal n, s x ∈ antidiagonal (m + n)
Tactic:
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ h
Proof state after:
case 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)
i j k l : ℕ
h : ((i, j), k, l) ∈ antidiagonal m ×ˢ antidiagonal n
⊢ s ((i, j), k, l) ∈ antidiagonal (m + n)
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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)
i j k l : ℕ
h : ((i, j), k, l) ∈ antidiagonal m ×ˢ antidiagonal n
⊢ s ((i, j), k, l) ∈ antidiagonal (m + n)
Tactic:
simp only [Finset.mem_antidiagonal, Finset.mem_product] at h ⊢
Proof state after:
case 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)
i j k l : ℕ
h : i + j = m ∧ k + l = n
⊢ i + k + (j + l) = m + n
Theorem: DividedPowers.IdealAdd.dpow_mul
Proof state before:
case 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)
i j k l : ℕ
h : i + j = m ∧ k + l = n
⊢ i + k + (j + l) = m + n
Tactic:
rw [add_assoc, ← add_assoc k j l, add_comm k _, add_assoc, h.2, ← add_assoc, h.1]
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)
⊢ ∑ 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
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 ∈ 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)
⊢ ∀ x ∈ antidiagonal (m + n),
    ∑ x ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (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_1 ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (antidiagonal m ×ˢ antidiagonal n),
              x.1.choose x_1.1.1 * x.2.choose x_1.1.2) *
          hI.dpow x.1 a *
        hJ.dpow x.2 b
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)
⊢ ∀ x ∈ antidiagonal (m + n),
    ∑ x ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (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_1 ∈ filter (fun x_1 => (fun x => s x) x_1 = x) (antidiagonal m ×ˢ antidiagonal n),
              x.1.choose x_1.1.1 * x.2.choose x_1.1.2) *
          hI.dpow x.1 a *
        hJ.dpow x.2 b
Tactic:
rintro ⟨u, v⟩ _
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 => (fun x => s x) 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 => (fun x => s x) x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
            (u, v).1.choose x.1.1 * (u, v).2.choose x.1.2) *
        hI.dpow (u, v).1 a *
      hJ.dpow (u, v).2 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 => (fun x => s x) 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 => (fun x => s x) x = (u, v)) (antidiagonal m ×ˢ antidiagonal n),
            (u, v).1.choose x.1.1 * (u, v).2.choose x.1.2) *
        hI.dpow (u, v).1 a *
      hJ.dpow (u, v).2 b
Tactic:
simp only [Prod.mk.injEq, mem_product, mem_antidiagonal, and_imp, Prod.forall, Nat.cast_sum, Nat.cast_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 =
    (∑ 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