case empty
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
⊢ Multiset.sum 0 ^ (↑Multiset.card 0 * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) 0))

case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ Multiset.sum (a ::ₘ s) ^ (↑Multiset.card (a ::ₘ s) * n + 1) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) (a ::ₘ s)))
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
s : Multiset α
n : ℕ
⊢ Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
induction' s using Multiset.induction_on with a s hs
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ ∑ m in Finset.range ((↑Multiset.card s + 1) * n + 1 + 1),
      a ^ m * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - m) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) m) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ Multiset.sum (a ::ₘ s) ^ (↑Multiset.card (a ::ₘ s) * n + 1) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) (a ::ₘ s)))
simp only [Finset.coe_insert, Multiset.map_cons, Multiset.toFinset_cons, Multiset.sum_cons,
  Multiset.card_cons, add_pow]
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ ∀ (c : ℕ),
    c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1) →
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
        span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ ∑ m in Finset.range ((↑Multiset.card s + 1) * n + 1 + 1),
      a ^ m * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - m) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) m) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
refine' Submodule.sum_mem _ _
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
⊢ ∀ (c : ℕ),
    c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1) →
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
        span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
intro c _hc
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)))
rw [mem_span_insert]
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z

case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
case cons
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
by_cases h : n + 1 ≤ c
no goals
case empty
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
⊢ Multiset.sum 0 ^ (↑Multiset.card 0 * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) 0))
simp
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
          ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) *
        a ^ (n + 1) +
      0
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
refine' ⟨a ^ (c - (n + 1)) * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) *
  ((Multiset.card s + 1) * n + 1).choose c, 0, Submodule.zero_mem _, _⟩
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (n + 1) *
        (a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
          ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c)) +
      0
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
          ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) *
        a ^ (n + 1) +
      0
rw [mul_comm _ (a ^ (n + 1))]
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
        ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) +
      0
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (n + 1) *
        (a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
          ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c)) +
      0
simp_rw [← mul_assoc]
no goals
case pos
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) *
        ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) +
      0
rw [← pow_add, add_zero, add_tsub_cancel_of_le h]
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        0 * a ^ (n + 1) + z
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ a_1 z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        a_1 * a ^ (n + 1) + z
use 0
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        z
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        0 * a ^ (n + 1) + z
simp_rw [zero_mul, zero_add]
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z,
    z ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s)) ∧
      a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) =
        z
refine' ⟨_, _, rfl⟩
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
replace h : c ≤ n := Nat.lt_succ_iff.mp (not_le.mp h)
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
have : (Multiset.card s + 1) * n + 1 - c = Multiset.card s * n + 1 + (n - c) := by
  rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * (Multiset.sum s ^ (↑Multiset.card s * n + 1) * Multiset.sum s ^ (n - c)) *
      ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * Multiset.sum s ^ ((↑Multiset.card s + 1) * n + 1 - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
rw [this, pow_add]
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * Multiset.sum s ^ (n - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) *
      Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * (Multiset.sum s ^ (↑Multiset.card s * n + 1) * Multiset.sum s ^ (n - c)) *
      ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
simp_rw [mul_assoc, mul_comm (s.sum ^ (Multiset.card s * n + 1)), ← mul_assoc]
no goals
case neg
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
this : (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
⊢ a ^ c * Multiset.sum s ^ (n - c) * ↑(Nat.choose ((↑Multiset.card s + 1) * n + 1) c) *
      Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈
    span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
exact mul_mem_left _ _ hs
no goals
α : Type u
β : Type v
a✝ b : α
inst✝ : CommSemiring α
I : Ideal α
n : ℕ
a : α
s : Multiset α
hs : Multiset.sum s ^ (↑Multiset.card s * n + 1) ∈ span ↑(Multiset.toFinset (Multiset.map (fun x => x ^ (n + 1)) s))
c : ℕ
_hc : c ∈ Finset.range ((↑Multiset.card s + 1) * n + 1 + 1)
h : c ≤ n
⊢ (↑Multiset.card s + 1) * n + 1 - c = ↑Multiset.card s * n + 1 + (n - c)
rw [add_mul, one_mul, add_assoc, add_comm n 1, ← add_assoc, add_tsub_assoc_of_le h]