theorem
proved
term proof
aggCoeff_flatMap
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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. -/