-- Mathlib/RingTheory/Ideal/Basic.lean
theorem pow_multiset_sum_mem_span_pow [DecidableEq α] (s : Multiset α) (n : ℕ) :
    s.sum ^ (Multiset.card s * n + 1) ∈
    span ((s.map fun (x : α) ↦ x ^ (n + 1)).toFinset : Set α)

Proof state:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
by_cases h : n + 1 ≤ c

Result:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

case neg
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Proof state:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset,
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = 0 * a ^ (n + 1) + z

Tactic:
simp_rw [zero_mul, zero_add]

Result:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : ¬n + 1 ≤ c
⊢ ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset,
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = z

Proof state:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z

Tactic:
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 _, ?_⟩

Result:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) * a ^ (n + 1) + 0

Proof state:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
⊢ ∑ m ∈ Finset.range ((s.card + 1) * n + 1 + 1),
      a ^ m * s.sum ^ ((s.card + 1) * n + 1 - m) * ↑(((s.card + 1) * n + 1).choose m) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)

Tactic:
refine Submodule.sum_mem _ ?_

Result:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
⊢ ∀ c ∈ Finset.range ((s.card + 1) * n + 1 + 1),
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
      span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)

Proof state:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ (n - c) * ↑(((s.card + 1) * n + 1).choose c) * s.sum ^ (s.card * n + 1) ∈
    span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset

Tactic:
exact mul_mem_left _ _ hs

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
⊢ s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset

Tactic:
induction' s using Multiset.induction_on with a s hs

Result:
case empty
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
⊢ Multiset.sum 0 ^ (Multiset.card 0 * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) 0).toFinset

case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
⊢ (a ::ₘ s).sum ^ ((a ::ₘ s).card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) (a ::ₘ s)).toFinset

Proof state:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
⊢ ∀ c ∈ Finset.range ((s.card + 1) * n + 1 + 1),
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
      span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)

Tactic:
intro c _hc

Result:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)

Proof state:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) * a ^ (n + 1) + 0

Tactic:
rw [mul_comm _ (a ^ (n + 1))]

Result:
case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * (a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c)) + 0