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
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:
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 =
    ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) 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 =
    ↑(Multiset.count i ↑k).factorial * ↑(mchoose (Multiset.count i ↑k) 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:
rw [mul_comm]
Proof state after:
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.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:
exact hJ.dpow_mem hi2' hb
Proof state after:
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.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 Submodule.mem_sup_left
Proof state after:
case neg.x.a
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
Theorem: DividedPowers.IdealAdd.dpow_comp_aux
Proof state before:
case neg.x.a
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
Tactic:
exact hI.dpow_mem hi1 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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
⊢ ∑ 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
Tactic:
rw [← Finset.sum_fiberwise_of_maps_to 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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
⊢ ∑ j ∈ range (m * n + 1),
      ∑ i ∈ filter (fun i => φ i = j) ((range (n + 1)).sym m),
        ∏ i_1 ∈ range (n + 1), dpow hI hJ (Multiset.count i_1 ↑i) (hI.dpow i_1 a * hJ.dpow (n - i_1) 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
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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
⊢ ∀ p ∈ range (m * n + 1),
    ∑ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
        ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
      ∑ k ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
        (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
                ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
              ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
            hI.dpow p a *
          hJ.dpow (m * n - p) b
Tactic:
intro p _
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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
⊢ ∑ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
      ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ k ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
      (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
              ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) 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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
⊢ ∑ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
      ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ k ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
      (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
              ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) 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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
⊢ ∀ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
    ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
      (∏ 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
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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
⊢ ∀ x ∈ filter (fun x => (fun k => φ k) x = p) ((range (n + 1)).sym m),
    ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b) =
      (∏ 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:
intro k hk
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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
k : Sym ℕ m
hk : k ∈ filter (fun x => (fun k => φ k) x = p) ((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) =
    (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
          ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
        hI.dpow p a *
      hJ.dpow (m * n - p) 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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
k : Sym ℕ m
hk : k ∈ filter (fun x => (fun k => φ k) x = p) ((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) =
    (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
          ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
        hI.dpow p a *
      hJ.dpow (m * n - p) b
Tactic:
rw [Finset.mem_filter] at hk
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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m ∧ (fun k => φ k) k = p
⊢ ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
          ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
        hI.dpow p a *
      hJ.dpow (m * n - p) 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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m ∧ (fun k => φ k) k = p
⊢ ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
          ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
        hI.dpow p a *
      hJ.dpow (m * n - p) b
Tactic:
rw [Finset.prod_congr rfl (L1 k), Finset.prod_mul_distrib, Finset.prod_mul_distrib,
  hI.prod_dpow_self _ ha, hJ.prod_dpow_self _ hb]
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
L1 :
  ∀ (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
φ : Sym ℕ m → ℕ := fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ_def : φ = fun k => ∑ i ∈ range (n + 1), Multiset.count i ↑k * i
hφ : ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
p : ℕ
x✝ : p ∈ range (m * n + 1)
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m ∧ (fun k => φ k) k = p
⊢ (∏ x ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n x ↑k)) *
        (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * x) *
          hI.dpow (∑ x ∈ range (n + 1), Multiset.count x ↑k * x) a) *
      (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) *
        hJ.dpow (∑ x ∈ range (n + 1), Multiset.count x ↑k * (n - x)) b) =
    (∏ i ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n i ↑k)) *
            ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * i) *
          ↑(Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑k * (n - i)) *
        hI.dpow p a *
      hJ.dpow (m * n - p) b