 372  simp only [List.filter_append, List.map_append, List.sum_append]
 373
 374/-- Aggregation over a flat-mapped list of row moves. -/
 375theorem aggCoeff_flatMap (nf : NormalForm) (pair : ℕ) (prim : Primitive)
 376    (l : List ℕ) (hl : l.Nodup) :
 377    aggCoeff (l.flatMap (rowMoves nf)) pair prim
 378      = if pair ∈ l then aggCoeff (rowMoves nf pair) pair prim else 0 := by
 379  induction l with
 380  | nil =>
 381    simp only [List.flatMap_nil, List.not_mem_nil, ↓reduceIte]
 382    unfold aggCoeff
 383    simp
 384  | cons h t ih =>
 385    simp only [List.flatMap_cons]
 386    rw [aggCoeff_append]
 387    have hnodup_t : t.Nodup := hl.of_cons
 388    have h_not_mem : h ∉ t := hl.not_mem
 389    by_cases hpair : pair = h
 390    · -- pair = h: contribution comes from rowMoves nf h, and pair ∉ t (since h ∉ t)
 391      subst hpair
 392      simp only [List.mem_cons, true_or, ↓reduceIte]
 393      have h_pair_not_in_t : pair ∉ t := h_not_mem
 394      rw [ih hnodup_t]
 395      simp only [h_pair_not_in_t, ↓reduceIte, add_zero]
 396    · -- pair ≠ h: contribution from rowMoves nf h is 0
 397      have h_ne : h ≠ pair := Ne.symm hpair
 398      rw [aggCoeff_rowMoves_of_ne nf h_ne]
 399      simp only [zero_add]
 400      rw [ih hnodup_t]
 401      -- pair ∈ h :: t ↔ pair = h ∨ pair ∈ t, but pair ≠ h, so pair ∈ h :: t ↔ pair ∈ t
 402      simp only [List.mem_cons, hpair, false_or]
 403
 404/-- Aggregated coefficient extracted from `toMoves` equals the canonical table. -/
 405lemma sumCoeffs_toMoves (nf : NormalForm) (pair : ℕ) (prim : Primitive) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.