internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ m (dpow hI hJ n (a + b)) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b
Tactic:
rw [dpow_eq hI hJ hIJ n ha hb, dpow_sum_aux (dpow hI hJ)]
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ (range (n + 1)).sym m, ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b

case dpow_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A
Tactic:
. intro x hx
  rw [dpow_zero hI hJ hIJ] exact hx
Proof state after:
case dpow_add
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case dpow_add
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
. simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
  intro n x y hx hy
  rw [dpow_add' hI hJ hIJ]
  exact hx
  exact hy
Proof state after:
case dpow_eval_zero
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
intro k i hi
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
simp only [cnik]
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
by_cases hi2 : i = n
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

case neg
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case neg
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
have hi2' : n - i ≠ 0 := by
  intro h; apply hi2
  rw [Finset.mem_range, Nat.lt_succ_iff] at hi
  rw [← Nat.sub_add_cancel hi, h, zero_add]
Proof state after:
case neg
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case neg
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
by_cases hi1 : i = 0
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

case neg
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
rw [hi2]
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow (n - n) b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else
              (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n *
                mchoose (Multiset.count n ↑k) (n - n)) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * (n - n)) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow (n - n) b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else
              (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n *
                mchoose (Multiset.count n ↑k) (n - n)) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * (n - n)) b
Tactic:
rw [Nat.sub_self]
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b
Tactic:
rw [if_neg hn]
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = n then mchoose (Multiset.count n ↑k) n
          else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = n then mchoose (Multiset.count n ↑k) n
          else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b
Tactic:
rw [if_pos rfl]
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a * hJ.dpow (Multiset.count n ↑k * 0) b
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a * hJ.dpow (Multiset.count n ↑k * 0) b
Tactic:
simp only [mchoose_zero', mul_one, Nat.cast_one, MulZeroClass.mul_zero, hJ.dpow_zero hb]
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a
Tactic:
rw [dpow_eq_of_mem_left hI hJ hIJ _ (hI.dpow_mem hn ha)]
Proof state after:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ hI.dpow (Multiset.count n ↑k) (hI.dpow n a) = ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case pos
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ hI.dpow (Multiset.count n ↑k) (hI.dpow n a) = ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a
Tactic:
rw [hI.dpow_comp _ hn ha]
Proof state after:
no goals
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
⊢ n - i ≠ 0
Tactic:
intro 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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
h : n - i = 0
⊢ False