`BookProof.ChapterF6.mgT_sum_add` (k : ℕ) (T : α →₀ ℕ) (s : List α) (hT : T.support.card ≤ k) : mgSum (mgT k T s) + (k + 1) * mgD k T s = mgSum T + s.length
ProvedBookProof.ChapterF6.mgT_sum_addtheoremstimepiece
Prove the following Lean 4 theorem from ChapterF6.
BookProof.ChapterF6.mgT_sum_add (k : ℕ) (T : α →₀ ℕ) (s : List α) (hT : T.support.card ≤ k) : mgSum (mgT k T s) + (k + 1) * mgD k T s = mgSum T + s.length
Formalization note: Lean 4 identifier BookProof.ChapterF6.mgT_sum_add.
Preamble
-- Generated from ChapterF6.lean — theorem BookProof.ChapterF6.mgT_sum_add
import Mathlib
import Definitions.Def_ChapterF6
open BookProof.ChapterF6
open scoped BigOperators
variable {α : Type*} [DecidableEq α]Formal statement
theorem BookProof.ChapterF6.mgT_sum_add (k : ℕ) (T : α →₀ ℕ) (s : List α) (hT : T.support.card ≤ k) :
mgSum (mgT k T s) + (k + 1) * mgD k T s = mgSum T + s.length := by sorry