English
The sum of select P x and select not P x equals x, i.e., select P x + select (not P) x = x.
Русский
Сумма select P x и select not P x равна x: select P x + select (¬P) x = x.
LaTeX
$$$ select\ P\ x + select\ (\lnot P)\ x = x $$$
Lean4
theorem select_add_select_not : ∀ x : 𝕎 R, select P x + select (fun i => ¬P i) x = x := by
-- Porting note: TC search was insufficient to find this instance, even though all required
-- instances exist. See zulip: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/WittVector.20saga/near/370073526]
have : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x := IsPoly₂.diag (hf := IsPoly₂.comp)
ghost_calc x
intro n
simp only [RingHom.map_add]
suffices
(bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
wittPolynomial p ℤ n
by
apply_fun aeval x.coeff at this
simpa only [map_add, aeval_bind₁, ← coeff_select]
simp only [wittPolynomial_eq_sum_C_mul_X_pow, selectPoly, map_sum, map_pow, map_mul, bind₁_X_right, bind₁_C_right,
← Finset.sum_add_distrib, ← mul_add]
apply Finset.sum_congr rfl
refine fun m _ => mul_eq_mul_left_iff.mpr (Or.inl ?_)
rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)]
by_cases Pm : P m
· rw [if_pos Pm, if_neg <| not_not_intro Pm, zero_pow Fin.pos'.ne', add_zero]
· rwa [if_neg Pm, if_pos, zero_add]
