Theorem: DividedPowers.IdealAdd.dpow_comp_aux (DividedPowers/IdealAdd.lean)

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ dpow hI hJ m (dpow hI hJ n (a + b)) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b
Tactic:
rw [dpow_eq hI hJ hIJ n ha hb, dpow_sum_aux (dpow hI hJ)]
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∑ k ∈ (range (n + 1)).sym m, ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b

case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A

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
⊢ ∑ k ∈ (range (n + 1)).sym m, ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b

case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A
Tactic:
set φ : Sym ℕ m → ℕ := fun k => (Finset.range (n + 1)).sum fun i => Multiset.count i ↑k * i
  with hφ_def
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 ∈ (range (n + 1)).sym m, ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b

case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A

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, ∏ i ∈ range (n + 1), dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ∑ p ∈ range (m * n + 1),
      ↑(∑ x ∈ filter (fun l => ∑ i ∈ range (n + 1), Multiset.count i ↑l * i = p) ((range (n + 1)).sym m),
              ((∏ i ∈ range (n + 1), DividedPowers.IdealAdd.cnik n i ↑x) *
                  Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * i) *
                Nat.multinomial (range (n + 1)) fun i => Multiset.count i ↑x * (n - i)) *
          hI.dpow p a *
        hJ.dpow (m * n - p) b

case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A
Tactic:
suffices hφ : ∀ k : Sym ℕ m, k ∈ (Finset.range (n + 1)).sym m → φ k ∈ Finset.range (m * n + 1) by
  rw [← Finset.sum_fiberwise_of_maps_to hφ _]
  suffices L4 :
    ∀ (p : ℕ) (_ : p ∈ Finset.range (m * n + 1)),
      ((Finset.filter (fun x : Sym ℕ m => (fun k : Sym ℕ m => φ k) x = p)
              ((Finset.range (n + 1)).sym m)).sum
          fun x : Sym ℕ m =>
          (Finset.range (n + 1)).prod fun i : ℕ =>
            dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b)) =
        (Finset.filter (fun x : Sym ℕ m => (fun k : Sym ℕ m => φ k) x = p)
              ((Finset.range (n + 1)).sym m)).sum
          fun k : Sym ℕ m =>
          ((Finset.range (n + 1)).prod fun i : ℕ => ↑(cnik n i ↑k)) *
                  ↑(Nat.multinomial (Finset.range (n + 1)) fun i : ℕ => Multiset.count i ↑k * i) *
                ↑(Nat.multinomial (Finset.range (n + 1)) fun i : ℕ =>
                    Multiset.count i ↑k * (n - i)) *
              hI.dpow p a *
            hJ.dpow (m * n - p) b by
      rw [Finset.sum_congr rfl L4]
      simp only [Sym.mem_coe, mem_sym_iff, mem_range, ge_iff_le, Nat.cast_sum, Nat.cast_mul,
      Nat.cast_prod]
      simp_rw [Finset.sum_mul]
  intro p _
  apply Finset.sum_congr rfl
  intro k hk
  rw [Finset.mem_filter] at hk
  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]
  simp only [mul_assoc]; apply congr_arg₂ _ rfl
  apply congr_arg₂ _ rfl
  rw [sum_range_sym_mul_compl hk.1]
  simp only [← mul_assoc]
  simp only [mem_sym_iff, mem_range, hφ_def] at hk
  rw [hk.2]
  apply congr_arg₂ _ _ rfl
  rw [mul_comm]
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 ∈ (range (n + 1)).sym m, φ k ∈ range (m * n + 1)

case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A

State before:
case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1

case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ ?m.65386 → y ∈ ?m.65386 → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ ?m.65386

A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ Ideal A
Tactic:
. intro x hx
  rw [dpow_zero hI hJ hIJ] exact hx
State after:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J

State before:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y

case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
. simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
  intro n x y hx hy
  rw [dpow_add' hI hJ hIJ]
  exact hx
  exact hy
State after:
case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0

case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (k : Sym ℕ m),
    ∀ i ∈ range (n + 1),
      dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
        ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
          hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
intro k i hi
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(DividedPowers.IdealAdd.cnik n i ↑k) * hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
simp only [cnik]
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
by_cases hi2 : i = n
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

State before:
case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
have hi2' : n - i ≠ 0 := by
  intro h; apply hi2
  rw [Finset.mem_range, Nat.lt_succ_iff] at hi
  rw [← Nat.sub_add_cancel hi, h, zero_add]
State after:
case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

State before:
case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
by_cases hi1 : i = 0
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
hi1 : i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

case neg
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
hi2' : n - i ≠ 0
hi1 : ¬i = 0
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count i ↑k) (hI.dpow i a * hJ.dpow (n - i) b) =
    ↑(if i = 0 then mchoose (Multiset.count i ↑k) n
          else
            if i = n then mchoose (Multiset.count i ↑k) n
            else
              (Multiset.count i ↑k).factorial * mchoose (Multiset.count i ↑k) i *
                mchoose (Multiset.count i ↑k) (n - i)) *
        hI.dpow (Multiset.count i ↑k * i) a *
      hJ.dpow (Multiset.count i ↑k * (n - i)) b
Tactic:
rw [hi2]
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow (n - n) b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else
              (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n *
                mchoose (Multiset.count n ↑k) (n - n)) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * (n - n)) b

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow (n - n) b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else
              (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n *
                mchoose (Multiset.count n ↑k) (n - n)) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * (n - n)) b
Tactic:
rw [Nat.sub_self]
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = 0 then mchoose (Multiset.count n ↑k) n
          else
            if n = n then mchoose (Multiset.count n ↑k) n
            else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b
Tactic:
rw [if_neg hn]
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = n then mchoose (Multiset.count n ↑k) n
          else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(if n = n then mchoose (Multiset.count n ↑k) n
          else (Multiset.count n ↑k).factorial * mchoose (Multiset.count n ↑k) n * mchoose (Multiset.count n ↑k) 0) *
        hI.dpow (Multiset.count n ↑k * n) a *
      hJ.dpow (Multiset.count n ↑k * 0) b
Tactic:
rw [if_pos rfl]
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a * hJ.dpow (Multiset.count n ↑k * 0) b

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a * hJ.dpow 0 b) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a * hJ.dpow (Multiset.count n ↑k * 0) b
Tactic:
simp only [mchoose_zero', mul_one, Nat.cast_one, MulZeroClass.mul_zero, hJ.dpow_zero hb]
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ dpow hI hJ (Multiset.count n ↑k) (hI.dpow n a) =
    ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a
Tactic:
rw [dpow_eq_of_mem_left hI hJ hIJ _ (hI.dpow_mem hn ha)]
State after:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ hI.dpow (Multiset.count n ↑k) (hI.dpow n a) = ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a

State before:
case pos
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : i = n
⊢ hI.dpow (Multiset.count n ↑k) (hI.dpow n a) = ↑(mchoose (Multiset.count n ↑k) n) * hI.dpow (Multiset.count n ↑k * n) a
Tactic:
rw [hI.dpow_comp _ hn ha]
State after:
no goals

State before:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
⊢ n - i ≠ 0
Tactic:
intro h
State after:
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
k : Sym ℕ m
i : ℕ
hi : i ∈ range (n + 1)
hi2 : ¬i = n
h : n - i = 0
⊢ False

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
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

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
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

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]
State after:
no goals

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]
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

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']
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

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]
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

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]
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

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]
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

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]
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

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)]
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

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]
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

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]
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

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]
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

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]
State after:
no goals

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]
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

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]
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

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]
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

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)]
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

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)]
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

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]
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

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]
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

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]
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

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
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

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]
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

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)]
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

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]
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

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
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

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]
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

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
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

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]
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

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
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

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
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

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
State after:
no goals

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φ _]
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

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)
⊢ ∑ 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
Tactic:
suffices L4 :
  ∀ (p : ℕ) (_ : p ∈ Finset.range (m * n + 1)),
    ((Finset.filter (fun x : Sym ℕ m => (fun k : Sym ℕ m => φ k) x = p)
            ((Finset.range (n + 1)).sym m)).sum
        fun x : Sym ℕ m =>
        (Finset.range (n + 1)).prod fun i : ℕ =>
          dpow hI hJ (Multiset.count i ↑x) (hI.dpow i a * hJ.dpow (n - i) b)) =
      (Finset.filter (fun x : Sym ℕ m => (fun k : Sym ℕ m => φ k) x = p)
            ((Finset.range (n + 1)).sym m)).sum
        fun k : Sym ℕ m =>
        ((Finset.range (n + 1)).prod fun i : ℕ => ↑(cnik n i ↑k)) *
                ↑(Nat.multinomial (Finset.range (n + 1)) fun i : ℕ => Multiset.count i ↑k * i) *
              ↑(Nat.multinomial (Finset.range (n + 1)) fun i : ℕ =>
                  Multiset.count i ↑k * (n - i)) *
            hI.dpow p a *
          hJ.dpow (m * n - p) b by
    rw [Finset.sum_congr rfl L4]
    simp only [Sym.mem_coe, mem_sym_iff, mem_range, ge_iff_le, Nat.cast_sum, Nat.cast_mul,
    Nat.cast_prod]
    simp_rw [Finset.sum_mul]
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 ∈ 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

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 _
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

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
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

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
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

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
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

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]
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

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]
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)))

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
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))

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
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)

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]
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)

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]
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

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
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

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]
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

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
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

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]
State after:
no goals

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
⊢ ∑ 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
Tactic:
rw [Finset.sum_congr rfl L4]
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)
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 => (fun k => φ k) 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 =
    ∑ 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

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 => (fun k => φ k) 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 =
    ∑ 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:
simp only [Sym.mem_coe, mem_sym_iff, mem_range, ge_iff_le, Nat.cast_sum, Nat.cast_mul,
Nat.cast_prod]
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)
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

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]
State after:
no goals

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
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)

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 : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m
⊢ φ k ∈ range (m * n + 1)
Tactic:
simp only [Sym.mem_coe, mem_range, Nat.lt_succ_iff]
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 ≤ m * n

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 : Sym ℕ m
hk : k ∈ (range (n + 1)).sym m
⊢ φ k ≤ m * n
Tactic:
exact range_sym_weighted_sum_le hk
State after:
no goals

State before:
case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {x : A}, x ∈ ?m.65386 → dpow hI hJ 0 x = 1
Tactic:
intro x hx
State after:
case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
x : A
hx : x ∈ ?m.65386
⊢ dpow hI hJ 0 x = 1

State before:
case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
x : A
hx : x ∈ ?m.65386
⊢ dpow hI hJ 0 x = 1
Tactic:
rw [dpow_zero hI hJ hIJ]
State after:
case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
x : A
hx : x ∈ ?m.65386
⊢ x ∈ I + J

State before:
case dpow_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
x : A
hx : x ∈ ?m.65386
⊢ x ∈ I + J
Tactic:
exact hx
State after:
no goals

State before:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ k ∈ antidiagonal n, dpow hI hJ k.1 x * dpow hI hJ k.2 y
Tactic:
simp only [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
State after:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ x_3 ∈ range n.succ, dpow hI hJ x_3 x * dpow hI hJ (n - x_3) y

State before:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ (n : ℕ) {x y : A},
    x ∈ I + J → y ∈ I + J → dpow hI hJ n (x + y) = ∑ x_3 ∈ range n.succ, dpow hI hJ x_3 x * dpow hI hJ (n - x_3) y
Tactic:
intro n x y hx hy
State after:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ dpow hI hJ n (x + y) = ∑ x_1 ∈ range n.succ, dpow hI hJ x_1 x * dpow hI hJ (n - x_1) y

State before:
case dpow_add
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n✝ : ℕ
hn : n✝ ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ dpow hI hJ n (x + y) = ∑ x_1 ∈ range n.succ, dpow hI hJ x_1 x * dpow hI hJ (n - x_1) y
Tactic:
rw [dpow_add' hI hJ hIJ]
State after:
case dpow_add.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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ x ∈ I + J

case dpow_add.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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J

State before:
case dpow_add.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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ x ∈ I + J

case dpow_add.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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J
Tactic:
exact hx
State after:
case dpow_add.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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J

State before:
case dpow_add.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
n : ℕ
x y : A
hx : x ∈ I + J
hy : y ∈ I + J
⊢ y ∈ I + J
Tactic:
exact hy
State after:
no goals

State before:
case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ {n : ℕ}, n ≠ 0 → dpow hI hJ n 0 = 0
Tactic:
intro n hn
State after:
case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n✝ : ℕ
hn✝ : n✝ ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
hn : n ≠ 0
⊢ dpow hI hJ n 0 = 0

State before:
case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n✝ : ℕ
hn✝ : n✝ ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
hn : n ≠ 0
⊢ dpow hI hJ n 0 = 0
Tactic:
rw [dpow_eq_of_mem_left hI hJ hIJ n I.zero_mem]
State after:
case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n✝ : ℕ
hn✝ : n✝ ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0

State before:
case dpow_eval_zero
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n✝ : ℕ
hn✝ : n✝ ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0
Tactic:
exact dpow_eval_zero hI hn
State after:
no goals

State before:
case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
⊢ ∀ i ∈ range (n + 1), hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
intro i _
State after:
case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J

State before:
case hx
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
by_cases hi0 : i = 0
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J

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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J

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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
rw [hi0]
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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ I + J

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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ I + J
Tactic:
apply Submodule.mem_sup_right
State after:
case pos.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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ J

State before:
case pos.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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hI.dpow 0 a * hJ.dpow (n - 0) b ∈ J
Tactic:
apply Ideal.mul_mem_left
State after:
case pos.a.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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hJ.dpow (n - 0) b ∈ J

State before:
case pos.a.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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : i = 0
⊢ hJ.dpow (n - 0) b ∈ J
Tactic:
exact hJ.dpow_mem hn hb
State after:
no goals

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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I + J
Tactic:
apply Submodule.mem_sup_left
State after:
case neg.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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I

State before:
case neg.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
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a * hJ.dpow (n - i) b ∈ I
Tactic:
apply Ideal.mul_mem_right
State after:
case neg.a.h
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a ∈ I

State before:
case neg.a.h
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
hIJ : ∀ (n : ℕ), ∀ a ∈ I ⊓ J, hI.dpow n a = hJ.dpow n a
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
b : A
hb : b ∈ J
i : ℕ
a✝ : i ∈ range (n + 1)
hi0 : ¬i = 0
⊢ hI.dpow i a ∈ I
Tactic:
exact hI.dpow_mem hi0 ha
State after:
no goals