internlm/Lean-Github huggingface dataset:
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) *
      (↑(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
Tactic:
rw [hI.dpow_comp _ 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
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * 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
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
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * 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
Tactic:
rw [hJ.dpow_comp _ hi2' hb]
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
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * i) a *
      (↑(Multiset.count i ↑k).factorial *
        (↑(mchoose (Multiset.count i ↑k) (n - i)) * hJ.dpow (Multiset.count i ↑k * (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
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
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * i) a *
      (↑(Multiset.count i ↑k).factorial *
        (↑(mchoose (Multiset.count i ↑k) (n - i)) * hJ.dpow (Multiset.count i ↑k * (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
Tactic:
simp only [← mul_assoc]
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
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * i) a * ↑(Multiset.count i ↑k).factorial *
        ↑(mchoose (Multiset.count i ↑k) (n - i)) *
      hJ.dpow (Multiset.count i ↑k * (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
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
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * i) a * ↑(Multiset.count i ↑k).factorial *
        ↑(mchoose (Multiset.count i ↑k) (n - i)) *
      hJ.dpow (Multiset.count i ↑k * (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
Tactic:
apply congr_arg₂ _ _ 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 : ℕ
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 i ↑k) i) * hI.dpow (Multiset.count i ↑k * i) a * ↑(Multiset.count i ↑k).factorial *
      ↑(mchoose (Multiset.count i ↑k) (n - i)) =
    ↑((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

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
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) * hI.dpow (Multiset.count i ↑k * i) a * ↑(Multiset.count i ↑k).factorial *
      ↑(mchoose (Multiset.count i ↑k) (n - i)) =
    ↑((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

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
Tactic:
simp only [mul_assoc]
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) *
      (hI.dpow (Multiset.count i ↑k * i) a *
        (↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)))) =
    ↑((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

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
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) *
      (hI.dpow (Multiset.count i ↑k * i) a *
        (↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)))) =
    ↑((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

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
Tactic:
rw [mul_comm (hI.dpow _ a)]
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) *
      (↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a) =
    ↑((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

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
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) *
      (↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a) =
    ↑((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

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
Tactic:
simp only [← mul_assoc]
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) * ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) *
      hI.dpow (Multiset.count i ↑k * i) a =
    ↑((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

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
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) * ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) *
      hI.dpow (Multiset.count i ↑k * i) a =
    ↑((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

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
Tactic:
apply congr_arg₂ _ _ 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 : ℕ
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 i ↑k) i) * ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) =
    ↑((Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i * mchoose (Multiset.count i ↑k) (n - i))

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
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) * ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) =
    ↑((Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i * mchoose (Multiset.count i ↑k) (n - i))

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
Tactic:
simp only [Sym.mem_coe, ge_iff_le, Nat.cast_mul]
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
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ ↑(mchoose (Multiset.count i ↑k) i) * ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) (n - i)) =
    ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) i) * ↑(mchoose (Multiset.count i ↑k) (n - i))

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