/-- **Parity lemma.** If `f` is an involution of a finite set `s`, then `s` and the set of fixed
points of `f` have the same parity. Proof by strong induction: remove a fixed point, or remove a
two-element orbit `{x, f x}`. (Mathlib has a more general version for any prime `p`:
`Equiv.Perm.card_fixedPoints_modEq`.) -/
theorem card_mod_two_of_involution {α : Type*} [DecidableEq α] (f : α → α) (s : Finset α)
(hmaps : ∀ x ∈ s, f x ∈ s) (hinv : ∀ x ∈ s, f (f x) = x) :
s.card % 2 = (s.filter (fun x => f x = x)).card % 2 := by
induction s using Finset.strongInduction with
| H s ih =>
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
· simp
by_cases hfx : f x = x
· -- Remove the fixed point `x`.
have hmaps' : ∀ y ∈ s.erase x, f y ∈ s.erase x := by
intro y hy
rw [mem_erase] at hy ⊢
refine ⟨fun hfy => hy.1 ?_, hmaps y hy.2⟩
calc y = f (f y) := (hinv y hy.2).symm
_ = x := by rw [hfy, hfx]
have IH := ih (s.erase x) (erase_ssubset hx) hmaps'
(fun y hy => hinv y (mem_of_mem_erase hy))
have hfilter : (s.erase x).filter (fun y => f y = y) =
(s.filter (fun y => f y = y)).erase x := by
ext y
simp only [mem_filter, mem_erase]
tauto
have h₁ := card_erase_add_one hx
have hxF : x ∈ s.filter (fun y => f y = y) := mem_filter.2 ⟨hx, hfx⟩
have h₂ := card_erase_add_one hxF
rw [hfilter] at IH
omega
· -- Remove the two-element orbit `{x, f x}`.
have hfxs : f x ∈ s.erase x := mem_erase.2 ⟨hfx, hmaps x hx⟩
have hmaps' : ∀ y ∈ (s.erase x).erase (f x), f y ∈ (s.erase x).erase (f x) := by
intro y hy
simp only [mem_erase] at hy ⊢
obtain ⟨hy₁, hy₂, hy₃⟩ := hy
refine ⟨fun h => hy₂ ?_, fun h => hy₁ ?_, hmaps y hy₃⟩
· calc y = f (f y) := (hinv y hy₃).symm
_ = x := by rw [h, hinv x hx]
· calc y = f (f y) := (hinv y hy₃).symm
_ = f x := by rw [h]
have IH := ih ((s.erase x).erase (f x))
((erase_ssubset hfxs).trans (erase_ssubset hx)) hmaps'
(fun y hy => hinv y (mem_of_mem_erase (mem_of_mem_erase hy)))
have hfilter : ((s.erase x).erase (f x)).filter (fun y => f y = y) =
s.filter (fun y => f y = y) := by
ext y
simp only [mem_filter, mem_erase]
constructor
· rintro ⟨⟨-, -, hy⟩, hfy⟩
exact ⟨hy, hfy⟩
· rintro ⟨hy, hfy⟩
refine ⟨⟨fun h => ?_, fun h => hfx (h ▸ hfy), hy⟩, hfy⟩
-- `f x` is not fixed, since `f (f x) = x ≠ f x`.
rw [h, hinv x hx] at hfy
exact hfx hfy.symm
have h₁ := card_erase_add_one hx
have h₂ := card_erase_add_one hfxs
rw [hfilter] at IH
omega