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
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
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
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))) =
    (∏ x ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n x ↑k)) *
      (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * x) *
        (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) *
          (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
⊢ (∏ 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))) =
    (∏ x ∈ range (n + 1), ↑(DividedPowers.IdealAdd.cnik n x ↑k)) *
      (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * x) *
        (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) *
          (hI.dpow p a * hJ.dpow (m * n - p) b)))
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
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
⊢ ↑(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)) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * x) *
      (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) *
        (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
⊢ ↑(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)) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * x) *
      (↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) *
        (hI.dpow p a * hJ.dpow (m * n - p) b))
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
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
⊢ 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) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * (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
⊢ 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) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * (hI.dpow p a * hJ.dpow (m * n - p) b)
Tactic:
rw [sum_range_sym_mul_compl hk.1]
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
⊢ 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 (m * n - ∑ i ∈ range (n + 1), Multiset.count i ↑k * i) b) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * (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
⊢ 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 (m * n - ∑ i ∈ range (n + 1), Multiset.count i ↑k * i) b) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * (hI.dpow p a * hJ.dpow (m * n - p) b)
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
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
⊢ 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 (m * n - ∑ x ∈ range (n + 1), Multiset.count x ↑k * x) b =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * 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
⊢ 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 (m * n - ∑ x ∈ range (n + 1), Multiset.count x ↑k * x) b =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hI.dpow p a * hJ.dpow (m * n - p) b
Tactic:
simp only [mem_sym_iff, mem_range, hφ_def] 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 : (∀ a ∈ k, a < n + 1) ∧ ∑ i ∈ range (n + 1), Multiset.count i ↑k * i = p
⊢ 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 (m * n - ∑ x ∈ range (n + 1), Multiset.count x ↑k * x) b =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * 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 : (∀ a ∈ k, a < n + 1) ∧ ∑ i ∈ range (n + 1), Multiset.count i ↑k * i = p
⊢ 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 (m * n - ∑ x ∈ range (n + 1), Multiset.count x ↑k * x) b =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hI.dpow p a * hJ.dpow (m * n - p) b
Tactic:
rw [hk.2]
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 : (∀ a ∈ k, a < n + 1) ∧ ∑ i ∈ range (n + 1), Multiset.count i ↑k * i = p
⊢ hI.dpow p a * ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hJ.dpow (m * n - p) b =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * 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 : (∀ a ∈ k, a < n + 1) ∧ ∑ i ∈ range (n + 1), Multiset.count i ↑k * i = p
⊢ hI.dpow p a * ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hJ.dpow (m * n - p) b =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hI.dpow p a * hJ.dpow (m * n - p) b
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
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 : (∀ a ∈ k, a < n + 1) ∧ ∑ i ∈ range (n + 1), Multiset.count i ↑k * i = p
⊢ hI.dpow p a * ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hI.dpow p a
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 : (∀ a ∈ k, a < n + 1) ∧ ∑ i ∈ range (n + 1), Multiset.count i ↑k * i = p
⊢ hI.dpow p a * ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) =
    ↑(Nat.multinomial (range (n + 1)) fun x => Multiset.count x ↑k * (n - x)) * hI.dpow p a
Tactic:
rw [mul_comm]
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)
L4 :
  ∀ 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
⊢ ∑ x ∈ range (m * n + 1),
      ∑ k ∈ filter (fun x_1 => φ x_1 = x) ((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 x a *
          hJ.dpow (m * n - x) b =
    ∑ x ∈ range (m * n + 1),
      (∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = x) ((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 x a *
        hJ.dpow (m * n - x) b
Tactic:
simp_rw [Finset.sum_mul]
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
⊢ ∀ k ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)
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
k : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m
⊢ φ k ∈ range (m * n + 1)