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
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
h : n - i = 0
⊢ False
Tactic:
apply hi2
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
⊢ i = n
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
h : n - i = 0
⊢ i = n
Tactic:
rw [Finset.mem_range, Nat.lt_succ_iff] at 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 ≤ n
hi2 : ¬i = n
h : n - i = 0
⊢ i = n
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 ≤ n
hi2 : ¬i = n
h : n - i = 0
⊢ i = n
Tactic:
rw [← Nat.sub_add_cancel hi, h, zero_add]
Proof state after:
no goals
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
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
Tactic:
rw [hi1]
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 0 ↑k) (hI.dpow 0 a * hJ.dpow (n - 0) b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else
              (Multiset.count 0 ↑k).factorial * mchoose (Multiset.count 0 ↑k) 0 *
                mchoose (Multiset.count 0 ↑k) (n - 0)) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * (n - 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (hI.dpow 0 a * hJ.dpow (n - 0) b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else
              (Multiset.count 0 ↑k).factorial * mchoose (Multiset.count 0 ↑k) 0 *
                mchoose (Multiset.count 0 ↑k) (n - 0)) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * (n - 0)) b
Tactic:
rw [mchoose_zero']
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 0 ↑k) (hI.dpow 0 a * hJ.dpow (n - 0) b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) (n - 0)) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * (n - 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (hI.dpow 0 a * hJ.dpow (n - 0) b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) (n - 0)) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * (n - 0)) b
Tactic:
rw [hI.dpow_zero 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (1 * hJ.dpow (n - 0) b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) (n - 0)) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * (n - 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (1 * hJ.dpow (n - 0) b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) (n - 0)) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * (n - 0)) b
Tactic:
rw [Nat.sub_zero]
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 0 ↑k) (1 * hJ.dpow n b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) n) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (1 * hJ.dpow n b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) n) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * n) b
Tactic:
rw [one_mul]
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 0 ↑k) (hJ.dpow n b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) n) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (hJ.dpow n b) =
    ↑(if 0 = 0 then mchoose (Multiset.count 0 ↑k) n
          else
            if 0 = n then mchoose (Multiset.count 0 ↑k) n
            else (Multiset.count 0 ↑k).factorial * 1 * mchoose (Multiset.count 0 ↑k) n) *
        hI.dpow (Multiset.count 0 ↑k * 0) a *
      hJ.dpow (Multiset.count 0 ↑k * n) 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (hJ.dpow n b) =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow (Multiset.count 0 ↑k * 0) a * hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count 0 ↑k) (hJ.dpow n b) =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow (Multiset.count 0 ↑k * 0) a * hJ.dpow (Multiset.count 0 ↑k * n) b
Tactic:
rw [dpow_eq_of_mem_right hI hJ hIJ _ (hJ.dpow_mem hn 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ hJ.dpow (Multiset.count 0 ↑k) (hJ.dpow n b) =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow (Multiset.count 0 ↑k * 0) a * hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ hJ.dpow (Multiset.count 0 ↑k) (hJ.dpow n b) =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow (Multiset.count 0 ↑k * 0) a * hJ.dpow (Multiset.count 0 ↑k * n) b
Tactic:
rw [hJ.dpow_comp _ hn 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ ↑(mchoose (Multiset.count 0 ↑k) n) * hJ.dpow (Multiset.count 0 ↑k * n) b =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow (Multiset.count 0 ↑k * 0) a * hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ ↑(mchoose (Multiset.count 0 ↑k) n) * hJ.dpow (Multiset.count 0 ↑k * n) b =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow (Multiset.count 0 ↑k * 0) a * hJ.dpow (Multiset.count 0 ↑k * n) b
Tactic:
rw [MulZeroClass.mul_zero]
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
⊢ ↑(mchoose (Multiset.count 0 ↑k) n) * hJ.dpow (Multiset.count 0 ↑k * n) b =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow 0 a * hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ ↑(mchoose (Multiset.count 0 ↑k) n) * hJ.dpow (Multiset.count 0 ↑k * n) b =
    ↑(mchoose (Multiset.count 0 ↑k) n) * hI.dpow 0 a * hJ.dpow (Multiset.count 0 ↑k * n) b
Tactic:
rw [hI.dpow_zero 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ ↑(mchoose (Multiset.count 0 ↑k) n) * hJ.dpow (Multiset.count 0 ↑k * n) b =
    ↑(mchoose (Multiset.count 0 ↑k) n) * 1 * hJ.dpow (Multiset.count 0 ↑k * 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
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ ↑(mchoose (Multiset.count 0 ↑k) n) * hJ.dpow (Multiset.count 0 ↑k * n) b =
    ↑(mchoose (Multiset.count 0 ↑k) n) * 1 * hJ.dpow (Multiset.count 0 ↑k * n) b
Tactic:
simp only [Nat.cast_one, one_mul, mul_one]
Proof state after:
no goals
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
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
Tactic:
rw [if_neg hi1]
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
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(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
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(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 [if_neg hi2]
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
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑((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
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑((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 [mul_comm, dpow_smul hI hJ hIJ, mul_comm]
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
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a) * hJ.dpow (n - i) b ^ Multiset.count i ↑k =
    ↑((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.x
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
⊢ hI.dpow i a ∈ I + J
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
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a) * hJ.dpow (n - i) b ^ Multiset.count i ↑k =
    ↑((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.x
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
⊢ hI.dpow i a ∈ I + J
Tactic:
rw [dpow_eq_of_mem_left hI hJ hIJ _ (hI.dpow_mem hi1 ha)]
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
hi1 : ¬i = 0
⊢ hI.dpow (Multiset.count i ↑k) (hI.dpow i a) * hJ.dpow (n - i) b ^ Multiset.count i ↑k =
    ↑((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.x
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
⊢ hI.dpow i a ∈ I + J
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
hi1 : ¬i = 0
⊢ hI.dpow (Multiset.count i ↑k) (hI.dpow i a) * hJ.dpow (n - i) b ^ Multiset.count i ↑k =
    ↑((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.x
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
⊢ hI.dpow i a ∈ I + J
Tactic:
rw [← hJ.factorial_mul_dpow_eq_pow (Multiset.count i k)]
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
hi1 : ¬i = 0
⊢ hI.dpow (Multiset.count i ↑k) (hI.dpow i a) *
      (↑(Multiset.count i ↑k).factorial * hJ.dpow (Multiset.count i ↑k) (hJ.dpow (n - i) b)) =
    ↑((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.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
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ hJ.dpow (n - i) b ∈ J

case neg.x
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
⊢ hI.dpow i a ∈ I + J