Grace/Cumulus/Combinatorics/DerangementCount.g17

Open in Workbench Download source

Imports

Partitions · DerangementFormula

Declarations

Source

1-- Counting derangements: the permutations of an n-element set without a2-- fixed point number d(n). A derangement p of S sends a chosen point a to3-- some b ≠ a; if p also sends b back to a, it is a derangement of the other4-- points, and otherwise composing with the transposition (a b) and5-- forgetting a leaves a derangement of S ∖ {a}. Both correspondences are6-- bijections, which gives the recurrence d(n + 2) = (n + 1)(d(n + 1) + d(n)).7-- Part of Cumulus, the Grace17 mathematics library.8-- Copyright (c) 2026 Grant Passmore.9-- Released under the Apache License 2.0. See LICENSE in the repository root.10-- Authors: Grant Passmore1112module Grace.Cumulus.Combinatorics.DerangementCount13import Partitions14import DerangementFormula1516-- The permutations of I without a fixed point.17def derangements (I : Set) : Set :=18  { p ∈ permutations(I) | ∀ x ∈ I, p(x) ≠ x }1920theorem derangements.permutation (I p : Set)21  requires member : p ∈ derangements(I)22  shows p ∈ permutations(I)23proof24  have parts := derangements.membership.forward with member25  exact parts.left2627theorem derangements.moves (I p x : Set)28  requires member : p ∈ derangements(I)29  requires hx : x ∈ I30  shows p(x) ≠ x31proof32  have parts := derangements.membership.forward with member33  exact parts.right with x, hx3435theorem derangements.subset (I : Set)36  shows derangements(I) ⊆ permutations(I)37proof38  intros p hp39  exact derangements.permutation with hp4041theorem derangements.finite (I : Set)42  requires finite : Finite(I)43  shows Finite(derangements(I))44proof45  exact Finite.subset with (permutations.finite with finite),46    (derangements.subset at I)4748-- On a finite set, an injective self-map without fixed points is a49-- derangement.50theorem derangements.of_injective (I p : Set)51  requires finite : Finite(I)52  requires injective : InjectiveBetween(p, I, I)53  requires moves : ∀ x ∈ I, p(x) ≠ x54  shows p ∈ derangements(I)55proof56  have permutation := permutations.of_injective with finite, injective57  exact derangements.membership.backward with ⟨permutation, moves⟩5859theorem derangements.function (I p : Set)60  requires member : p ∈ derangements(I)61  shows p : I → I62proof63  exact permutations.function with (derangements.permutation with member)6465theorem derangements.apply_closed (I p x : Set)66  requires member : p ∈ derangements(I)67  requires hx : x ∈ I68  shows p(x) ∈ I69proof70  exact permutations.apply_closed with71    (derangements.permutation with member), hx7273theorem derangements.apply_cancel (I p x y : Set)74  requires member : p ∈ derangements(I)75  requires hx : x ∈ I76  requires hy : y ∈ I77  requires same : p(x) = p(y)78  shows x = y79proof80  exact permutations.apply_cancel with81    (derangements.permutation with member), hx, hy, same8283-- The empty set has one derangement, a singleton none.84theorem derangements.empty85  shows derangements(∅) = {∅}86proof87  ext p88  constructor89  . intro member90    have permutation := derangements.permutation with member91    rw permutations.empty at permutation92    exact permutation93  . intro member94    have equal := singleton.membership.forward with member95    rw equal96    apply derangements.membership.backward97    constructor98    . rw permutations.empty99      exact singleton.self at ∅100    . intros x hx101      exfalso102      exact set.empty with hx103104theorem derangements.empty_count105  shows cardinality(derangements(∅)) = 1106proof107  rw derangements.empty108  exact cardinality.singleton at ∅109110theorem derangements.singleton (x : Set)111  shows derangements({x}) = ∅112proof113  apply Subset.empty_iff.forward114  intros p hp115  have self := singleton.self at x116  have value := derangements.apply_closed with hp, self117  have same := singleton.membership.forward with value118  exfalso119  exact derangements.moves with hp, self, same120121theorem derangements.singleton_count (x : Set)122  shows cardinality(derangements({x})) = 0123proof124  rw derangements.singleton125  exact cardinality.empty126127-- The values of an extended map.128theorem adjoinMap.apply_new (f A B a b : Set)129  requires hf : f : A → B130  requires ha : ¬a ∈ A131  shows adjoinMap(f, a, b)(a) = b132proof133  have function := adjoinMap.function at f, A, B, a, b with hf, ha134  exact FunctionBetween.apply_value with function, (insert.self at a, A),135    (adjoinMap.relates_new at f, a, b)136137theorem adjoinMap.apply_old (f A B a b x : Set)138  requires hf : f : A → B139  requires ha : ¬a ∈ A140  requires hx : x ∈ A141  shows adjoinMap(f, a, b)(x) = f(x)142proof143  have function := adjoinMap.function at f, A, B, a, b with hf, ha144  have related := adjoinMap.relates_old at f, a, b, x, f(x) with145    (FunctionBetween.relates_apply with hf, hx)146  exact FunctionBetween.apply_value with function, (insert.contains with hx),147    related148149-- The derangements of S sending a to b, split by whether b returns to a.150151def swapFiber (S a b : Set) : Set :=152  { p ∈ derangements(S) | p(a) = b ∧ p(b) = a }153154def throughFiber (S a b : Set) : Set :=155  { p ∈ derangements(S) | p(a) = b ∧ p(b) ≠ a }156157theorem swapFiber.subset (S a b : Set)158  shows swapFiber(S, a, b) ⊆ derangements(S)159proof160  intros p hp161  have parts := swapFiber.membership.forward with hp162  exact parts.left163164theorem throughFiber.subset (S a b : Set)165  shows throughFiber(S, a, b) ⊆ derangements(S)166proof167  intros p hp168  have parts := throughFiber.membership.forward with hp169  exact parts.left170171theorem swapFiber.disjoint (S a b : Set)172  shows Disjoint(swapFiber(S, a, b), throughFiber(S, a, b))173proof174  apply Disjoint.iff.backward175  intros p inSwap inThrough176  have swap := swapFiber.membership.forward with inSwap177  have through := throughFiber.membership.forward with inThrough178  exact through.right.right with swap.right.right179180-- The value at a, as a map into S ∖ {a}.181defgraph valueAt (S a : Set) (p ∈ derangements(S)) : S ∖ {a} := p(a)182requires ha : a ∈ S183proof184  have inS := derangements.apply_closed with member, ha185  have moved := derangements.moves with member, ha186  exact difference.singleton_membership.backward with ⟨inS, moved⟩187188theorem valueAt.preimage (S a b : Set)189  requires ha : a ∈ S190  shows functionPreimage(valueAt(S, a), derangements(S), {b}) =191    swapFiber(S, a, b) ∪ throughFiber(S, a, b)192proof193  ext p194  constructor195  . intro hp196    obtain ⟨member, value⟩ := functionPreimage.point_membership.forward with hp197    have shape := valueAt.value at S, a, p with ha, member198    rw shape at value199    have alternatives : p(b) = a ∨ p(b) ≠ a by tauto200    cases alternatives with back | onward201    . apply union2.left202      exact swapFiber.membership.backward with ⟨member, value, back⟩203    . apply union2.right204      exact throughFiber.membership.backward with ⟨member, value, onward⟩205  . intro hp206    have split := union2.membership.forward with hp207    apply functionPreimage.point_membership.backward208    cases split with inSwap | inThrough209    . obtain ⟨member, value, back⟩ := swapFiber.membership.forward with inSwap210      have shape := valueAt.value at S, a, p with ha, member211      rw shape212      exact ⟨member, value⟩213    . obtain ⟨member, value, onward⟩ :=214        throughFiber.membership.forward with inThrough215      have shape := valueAt.value at S, a, p with ha, member216      rw shape217      exact ⟨member, value⟩218219-- Derangements exchanging a and b are the derangements of the other points.220221theorem difference.pair_subset (S a b : Set)222  shows (S ∖ {a}) ∖ {b} ⊆ S223proof224  exact Subset.transitive with (difference.subset_left at S ∖ {a}, {b}),225    (difference.subset_left at S, {a})226227theorem difference.pair_membership (S a b x : Set)228  shows x ∈ (S ∖ {a}) ∖ {b} ↔ x ∈ S ∧ x ≠ a ∧ x ≠ b229proof230  simp [difference.singleton_membership]231232defgraph swapRestrict (S a b : Set) (p ∈ swapFiber(S, a, b)) :233    derangements((S ∖ {a}) ∖ {b}) :=234  restrict(p, (S ∖ {a}) ∖ {b})235requires finite : Finite(S)236requires ha : a ∈ S237requires hb : b ∈ S238proof239  obtain ⟨hp, pa, pb⟩ := swapFiber.membership.forward with member240  have function := derangements.function with hp241  have injective := Bijective.injective with242    (permutations.bijective with (derangements.permutation with hp))243  have subset := difference.pair_subset at S, a, b244  have restricted := restrict.injective with injective, subset245  have values : ∀ x ∈ (S ∖ {a}) ∖ {b},246      restrict(p, (S ∖ {a}) ∖ {b})(x) ∈ (S ∖ {a}) ∖ {b}247    intros x hx248    have step := restrict.domain_apply with function, subset, hx249    rw step250    obtain ⟨xInS, xNotA, xNotB⟩ := difference.pair_membership.forward with hx251    have pxIn := derangements.apply_closed with hp, xInS252    apply difference.pair_membership.backward253    refine ⟨pxIn, ?_, ?_⟩254    . intro same255      have equal : p(x) = p(b)256        rw [same, pb]257        rfl258      exact xNotB with (derangements.apply_cancel with hp, xInS, hb, equal)259    . intro same260      have equal : p(x) = p(a)261        rw [same, pa]262        rfl263      exact xNotA with (derangements.apply_cancel with hp, xInS, ha, equal)264  have narrowed := FunctionBetween.codomain_of_values with265    (Injective.function with restricted), values266  have injectiveRest : InjectiveBetween(restrict(p, (S ∖ {a}) ∖ {b}),267      (S ∖ {a}) ∖ {b}, (S ∖ {a}) ∖ {b})268    apply Injective.of_pointwise with narrowed269    intros x hx y hy same270    exact Injective.apply_cancel with restricted, hx, hy, same271  have moves : ∀ x ∈ (S ∖ {a}) ∖ {b}, restrict(p, (S ∖ {a}) ∖ {b})(x) ≠ x272    intros x hx273    have step := restrict.domain_apply with function, subset, hx274    rw step275    exact derangements.moves with hp, (subset with x, hx)276  exact derangements.of_injective with (Finite.subset with finite, subset),277    injectiveRest, moves278279theorem swapRestrict.injective (S a b : Set)280  requires finite : Finite(S)281  requires ha : a ∈ S282  requires hb : b ∈ S283  shows InjectiveBetween(swapRestrict(S, a, b), swapFiber(S, a, b),284    derangements((S ∖ {a}) ∖ {b}))285proof286  have graph := swapRestrict.function at S, a, b with finite, ha, hb287  have subset := difference.pair_subset at S, a, b288  apply Injective.of_pointwise with graph289  intros p hp q hq same290  obtain ⟨pIn, pa, pb⟩ := swapFiber.membership.forward with hp291  obtain ⟨qIn, qa, qb⟩ := swapFiber.membership.forward with hq292  have pFunction := derangements.function with pIn293  have qFunction := derangements.function with qIn294  have valueP := swapRestrict.value at S, a, b, p with finite, ha, hb, hp295  have valueQ := swapRestrict.value at S, a, b, q with finite, ha, hb, hq296  rw [valueP, valueQ] at same297  apply FunctionBetween.ext with pFunction, qFunction298  intros x hx299  have alternatives : x = a ∨ x = b ∨ (x ≠ a ∧ x ≠ b) by tauto300  cases alternatives with isA | rest301  . rw [isA, pa, qa]302    rfl303  . cases rest with isB | other304    . rw [isB, pb, qb]305      rfl306    . have inRest : x ∈ (S ∖ {a}) ∖ {b} :=307        difference.pair_membership.backward with ⟨hx, other.left, other.right⟩308      have stepP := restrict.domain_apply with pFunction, subset, inRest309      have stepQ := restrict.domain_apply with qFunction, subset, inRest310      rw [← stepP, ← stepQ, same]311      rfl312313-- Adjoining a ↦ b and b ↦ a to a derangement of the other points.314315def swapExtend (q a b : Set) : Set := adjoinMap(adjoinMap(q, a, b), b, a)316317section SwapExtension318variable (S a b q : Set)319hypothesis finite : Finite(S)320hypothesis ha : a ∈ S321hypothesis hb : b ∈ S322hypothesis distinct : a ≠ b323hypothesis hq : q ∈ derangements((S ∖ {a}) ∖ {b})324325theorem swapExtend.injective326  shows InjectiveBetween(swapExtend(q, a, b), S, S)327proof328  have qInjective := Bijective.injective with329    (permutations.bijective with (derangements.permutation with hq))330  have aOut : ¬a ∈ (S ∖ {a}) ∖ {b}331    intro inside332    have parts := difference.pair_membership.forward with inside333    apply parts.right.left334    rfl335  have bOut : ¬b ∈ (S ∖ {a}) ∖ {b}336    intro inside337    have parts := difference.pair_membership.forward with inside338    apply parts.right.right339    rfl340  have first := adjoinMap.injective with qInjective, aOut, bOut341  have bOutA : ¬b ∈ insert(a, (S ∖ {a}) ∖ {b})342    intro inside343    have split := insert.membership.forward with inside344    cases split with same | inRest345    . apply distinct346      symm347      exact same348    . exact bOut with inRest349  have aOutB : ¬a ∈ insert(b, (S ∖ {a}) ∖ {b})350    intro inside351    have split := insert.membership.forward with inside352    cases split with same | inRest353    . exact distinct with same354    . exact aOut with inRest355  have second := adjoinMap.injective with first, bOutA, aOutB356  have domain : insert(b, insert(a, (S ∖ {a}) ∖ {b})) = S357    ext x358    simp [insert.membership, difference.pair_membership]359  have codomain : insert(a, insert(b, (S ∖ {a}) ∖ {b})) = S360    ext x361    simp [insert.membership, difference.pair_membership]362  rw [domain, codomain] at second363  unfold swapExtend364  exact second365366theorem swapExtend.apply_second367  shows swapExtend(q, a, b)(b) = a368proof369  have qFunction := derangements.function with hq370  have aOut : ¬a ∈ (S ∖ {a}) ∖ {b}371    intro inside372    have parts := difference.pair_membership.forward with inside373    apply parts.right.left374    rfl375  have bOutA : ¬b ∈ insert(a, (S ∖ {a}) ∖ {b})376    intro inside377    have split := insert.membership.forward with inside378    cases split with same | inRest379    . apply distinct380      symm381      exact same382    . have parts := difference.pair_membership.forward with inRest383      apply parts.right.right384      rfl385  have firstFunction := adjoinMap.function at q, (S ∖ {a}) ∖ {b},386    (S ∖ {a}) ∖ {b}, a, b with qFunction, aOut387  unfold swapExtend388  exact adjoinMap.apply_new at adjoinMap(q, a, b), insert(a, (S ∖ {a}) ∖ {b}),389    insert(b, (S ∖ {a}) ∖ {b}), b, a with firstFunction, bOutA390391theorem swapExtend.apply_first392  shows swapExtend(q, a, b)(a) = b393proof394  have qFunction := derangements.function with hq395  have aOut : ¬a ∈ (S ∖ {a}) ∖ {b}396    intro inside397    have parts := difference.pair_membership.forward with inside398    apply parts.right.left399    rfl400  have bOutA : ¬b ∈ insert(a, (S ∖ {a}) ∖ {b})401    intro inside402    have split := insert.membership.forward with inside403    cases split with same | inRest404    . apply distinct405      symm406      exact same407    . have parts := difference.pair_membership.forward with inRest408      apply parts.right.right409      rfl410  have firstFunction := adjoinMap.function at q, (S ∖ {a}) ∖ {b},411    (S ∖ {a}) ∖ {b}, a, b with qFunction, aOut412  have aIn : a ∈ insert(a, (S ∖ {a}) ∖ {b}) := insert.self at a, (S ∖ {a}) ∖ {b}413  have outer : swapExtend(q, a, b)(a) = adjoinMap(q, a, b)(a)414    unfold swapExtend415    exact adjoinMap.apply_old at adjoinMap(q, a, b),416      insert(a, (S ∖ {a}) ∖ {b}), insert(b, (S ∖ {a}) ∖ {b}), b, a, a with417      firstFunction, bOutA, aIn418  have inner := adjoinMap.apply_new at q, (S ∖ {a}) ∖ {b}, (S ∖ {a}) ∖ {b},419    a, b with qFunction, aOut420  rw [outer, inner]421  rfl422423theorem swapExtend.apply_rest (x : Set)424  requires hx : x ∈ (S ∖ {a}) ∖ {b}425  shows swapExtend(q, a, b)(x) = q(x)426proof427  have qFunction := derangements.function with hq428  have aOut : ¬a ∈ (S ∖ {a}) ∖ {b}429    intro inside430    have parts := difference.pair_membership.forward with inside431    apply parts.right.left432    rfl433  have bOutA : ¬b ∈ insert(a, (S ∖ {a}) ∖ {b})434    intro inside435    have split := insert.membership.forward with inside436    cases split with same | inRest437    . apply distinct438      symm439      exact same440    . have parts := difference.pair_membership.forward with inRest441      apply parts.right.right442      rfl443  have firstFunction := adjoinMap.function at q, (S ∖ {a}) ∖ {b},444    (S ∖ {a}) ∖ {b}, a, b with qFunction, aOut445  have xIn : x ∈ insert(a, (S ∖ {a}) ∖ {b}) := insert.contains with hx446  have outer : swapExtend(q, a, b)(x) = adjoinMap(q, a, b)(x)447    unfold swapExtend448    exact adjoinMap.apply_old at adjoinMap(q, a, b),449      insert(a, (S ∖ {a}) ∖ {b}), insert(b, (S ∖ {a}) ∖ {b}), b, a, x with450      firstFunction, bOutA, xIn451  have inner := adjoinMap.apply_old at q, (S ∖ {a}) ∖ {b}, (S ∖ {a}) ∖ {b},452    a, b, x with qFunction, aOut, hx453  rw [outer, inner]454  rfl455456theorem swapExtend.member457  shows swapExtend(q, a, b) ∈ swapFiber(S, a, b)458proof459  have injective := swapExtend.injective at S, a, b, q with *460  have atA := swapExtend.apply_first at S, a, b, q with *461  have atB := swapExtend.apply_second at S, a, b, q with *462  have moves : ∀ x ∈ S, swapExtend(q, a, b)(x) ≠ x463    intros x hx464    have alternatives : x = a ∨ x = b ∨ (x ≠ a ∧ x ≠ b) by tauto465    cases alternatives with isA | rest466    . rw [isA, atA]467      intro same468      apply distinct469      symm470      exact same471    . cases rest with isB | other472      . rw [isB, atB]473        exact distinct474      . have inRest : x ∈ (S ∖ {a}) ∖ {b} :=475          difference.pair_membership.backward with ⟨hx, other.left, other.right⟩476        have value := swapExtend.apply_rest at S, a, b, q, x with *477        rw value478        exact derangements.moves with hq, inRest479  have deranged := derangements.of_injective with finite, injective, moves480  exact swapFiber.membership.backward with ⟨deranged, atA, atB⟩481482end SwapExtension483484theorem swapRestrict.surjective (S a b : Set)485  requires finite : Finite(S)486  requires ha : a ∈ S487  requires hb : b ∈ S488  requires distinct : a ≠ b489  shows SurjectiveBetween(swapRestrict(S, a, b), swapFiber(S, a, b),490    derangements((S ∖ {a}) ∖ {b}))491proof492  have graph := swapRestrict.function at S, a, b with finite, ha, hb493  have subset := difference.pair_subset at S, a, b494  unfold SurjectiveBetween495  refine ⟨graph, ?_⟩496  intros q hq497  have inFiber := swapExtend.member at S, a, b, q with *498  refine ⟨swapExtend(q, a, b), inFiber, ?_⟩499  have value := swapRestrict.value at S, a, b, swapExtend(q, a, b) with500    finite, ha, hb, inFiber501  have restored : restrict(swapExtend(q, a, b), (S ∖ {a}) ∖ {b}) = q502    have pFunction := Injective.function with503      (swapExtend.injective at S, a, b, q with *)504    have inImage := swapRestrict.closed at S, a, b, swapExtend(q, a, b) with505      finite, ha, hb, inFiber506    have mapped := derangements.function at (S ∖ {a}) ∖ {b},507      restrict(swapExtend(q, a, b), (S ∖ {a}) ∖ {b}) with inImage508    have qFunction := derangements.function at (S ∖ {a}) ∖ {b}, q with hq509    apply FunctionBetween.ext with mapped, qFunction510    intros x hx511    have step := restrict.domain_apply with pFunction, subset, hx512    rw step513    exact swapExtend.apply_rest at S, a, b, q, x with *514  have related := FunctionBetween.relates_apply with graph, inFiber515  rw [value, restored] at related516  exact related517518theorem swapFiber.count (S a b : Set)519  requires finite : Finite(S)520  requires ha : a ∈ S521  requires hb : b ∈ S522  requires distinct : a ≠ b523  shows cardinality(swapFiber(S, a, b)) =524    cardinality(derangements((S ∖ {a}) ∖ {b}))525proof526  have injective := swapRestrict.injective with finite, ha, hb527  have surjective := swapRestrict.surjective with finite, ha, hb, distinct528  have finiteFiber := Finite.subset with (derangements.finite with finite),529    (swapFiber.subset at S, a, b)530  have bijective : BijectiveBetween(swapRestrict(S, a, b), swapFiber(S, a, b),531    derangements((S ∖ {a}) ∖ {b})) := ⟨injective, surjective⟩532  exact cardinality.bijective with finiteFiber, bijective533534-- Derangements sending a to b without return correspond to the derangements535-- of S ∖ {a}: compose with the transposition (a b) and forget a.536537theorem transposition.apply_closed (S a b x : Set)538  requires ha : a ∈ S539  requires hb : b ∈ S540  requires hx : x ∈ S541  shows transposition(S, a, b)(x) ∈ S542proof543  have function := transposition.function at S, a, b with ha, hb544  exact FunctionBetween.apply_closed with function, hx545546theorem transposition.apply_cancel (S a b x y : Set)547  requires ha : a ∈ S548  requires hb : b ∈ S549  requires hx : x ∈ S550  requires hy : y ∈ S551  requires same : transposition(S, a, b)(x) = transposition(S, a, b)(y)552  shows x = y553proof554  have bijective := transposition.bijective at S, a, b with ha, hb555  exact Injective.apply_cancel with (Bijective.injective with bijective),556    hx, hy, same557558-- The map x ↦ (a b)(p(x)) on S ∖ {a}.559def throughMap (S a b p : Set) : Set :=560  restrict(compose(transposition(S, a, b), p, S, S, S), S ∖ {a})561562theorem throughMap.apply (S a b p x : Set)563  requires ha : a ∈ S564  requires hb : b ∈ S565  requires function : p : S → S566  requires hx : x ∈ S ∖ {a}567  shows throughMap(S, a, b, p)(x) = transposition(S, a, b)(p(x))568proof569  have subset := difference.subset_left at S, {a}570  have tauFunction := transposition.function at S, a, b with ha, hb571  have composed := compose.function with function, tauFunction572  have step := restrict.domain_apply with composed, subset, hx573  have inner := compose.apply with function, tauFunction, (subset with x, hx)574  simp [throughMap]575576defgraph throughRestrict (S a b : Set) (p ∈ throughFiber(S, a, b)) :577    derangements(S ∖ {a}) :=578  throughMap(S, a, b, p)579requires finite : Finite(S)580requires ha : a ∈ S581requires hb : b ∈ S582proof583  obtain ⟨hp, pa, pb⟩ := throughFiber.membership.forward with member584  have function := derangements.function with hp585  have permutation := derangements.permutation with hp586  have tauPermutation := permutations.transposition at S, a, b with ha, hb587  have composed := permutations.compose with permutation, tauPermutation588  have subset := difference.subset_left at S, {a}589  have restricted : InjectiveBetween(throughMap(S, a, b, p), S ∖ {a}, S)590    unfold throughMap591    exact restrict.injective with592      (Bijective.injective with (permutations.bijective with composed)), subset593  have tauB := transposition.second at S, a, b with ha, hb594  have tauA := transposition.first at S, a, b with ha, hb595  have values : ∀ x ∈ S ∖ {a}, throughMap(S, a, b, p)(x) ∈ S ∖ {a}596    intros x hx597    have rewrite := throughMap.apply with ha, hb, function, hx598    rw rewrite599    obtain ⟨xInS, xNotA⟩ := difference.singleton_membership.forward with hx600    have pxIn := derangements.apply_closed with hp, xInS601    have tauIn := transposition.apply_closed with ha, hb, pxIn602    apply difference.singleton_membership.backward603    refine ⟨tauIn, ?_⟩604    intro same605    have equal : transposition(S, a, b)(p(x)) = transposition(S, a, b)(b)606      rw [same, tauB]607      rfl608    have pxB := transposition.apply_cancel with ha, hb, pxIn, hb, equal609    have equalA : p(x) = p(a)610      rw [pxB, pa]611      rfl612    exact xNotA with (derangements.apply_cancel with hp, xInS, ha, equalA)613  have narrowed := FunctionBetween.codomain_of_values with614    (Injective.function with restricted), values615  have injectiveRest : InjectiveBetween(throughMap(S, a, b, p), S ∖ {a},616      S ∖ {a})617    apply Injective.of_pointwise with narrowed618    intros x hx y hy same619    exact Injective.apply_cancel with restricted, hx, hy, same620  have moves : ∀ x ∈ S ∖ {a}, throughMap(S, a, b, p)(x) ≠ x621    intros x hx622    have rewrite := throughMap.apply with ha, hb, function, hx623    rw rewrite624    obtain ⟨xInS, xNotA⟩ := difference.singleton_membership.forward with hx625    have pxIn := derangements.apply_closed with hp, xInS626    intro same627    have alternatives : p(x) = a ∨ p(x) = b ∨ (p(x) ≠ a ∧ p(x) ≠ b) by tauto628    cases alternatives with isA | rest629    . rw [isA, tauA] at same630      apply pb631      rw same632      exact isA633    . cases rest with isB | other634      . have equal : p(x) = p(a)635          rw [isB, pa]636          rfl637        exact xNotA with (derangements.apply_cancel with hp, xInS, ha, equal)638      . have fixed := transposition.other at S, a, b, p(x) with639          ha, hb, pxIn, other.left, other.right640        rw fixed at same641        exact derangements.moves with hp, xInS, same642  exact derangements.of_injective with (Finite.subset with finite, subset),643    injectiveRest, moves644645theorem throughRestrict.injective (S a b : Set)646  requires finite : Finite(S)647  requires ha : a ∈ S648  requires hb : b ∈ S649  shows InjectiveBetween(throughRestrict(S, a, b), throughFiber(S, a, b),650    derangements(S ∖ {a}))651proof652  have graph := throughRestrict.function at S, a, b with finite, ha, hb653  apply Injective.of_pointwise with graph654  intros p hp q hq same655  obtain ⟨pIn, pa, pb⟩ := throughFiber.membership.forward with hp656  obtain ⟨qIn, qa, qb⟩ := throughFiber.membership.forward with hq657  have pFunction := derangements.function with pIn658  have qFunction := derangements.function with qIn659  have valueP := throughRestrict.value at S, a, b, p with finite, ha, hb, hp660  have valueQ := throughRestrict.value at S, a, b, q with finite, ha, hb, hq661  rw [valueP, valueQ] at same662  apply FunctionBetween.ext with pFunction, qFunction663  intros x hx664  have alternatives : x = a ∨ x ≠ a by tauto665  cases alternatives with isA | notA666  . rw [isA, pa, qa]667    rfl668  . have inRest : x ∈ S ∖ {a} :=669      difference.singleton_membership.backward with ⟨hx, notA⟩670    have stepP := throughMap.apply with ha, hb, pFunction, inRest671    have stepQ := throughMap.apply with ha, hb, qFunction, inRest672    rw same at stepP673    have equal : transposition(S, a, b)(p(x)) = transposition(S, a, b)(q(x))674      rw [← stepP, ← stepQ]675      rfl676    have pxIn := derangements.apply_closed with pIn, hx677    have qxIn := derangements.apply_closed with qIn, hx678    exact transposition.apply_cancel with ha, hb, pxIn, qxIn, equal679680-- Adjoining a ↦ b to x ↦ (a b)(r(x)) recovers a derangement of S that681-- sends a to b and does not send b back.682683def throughLift (S a b r : Set) : Set :=684  compose(restrict(transposition(S, a, b), S ∖ {a}), r, S ∖ {a}, S ∖ {a}, S)685686def throughExtend (S a b r : Set) : Set :=687  adjoinMap(throughLift(S, a, b, r), a, b)688689section ThroughExtension690variable (S a b r : Set)691hypothesis finite : Finite(S)692hypothesis ha : a ∈ S693hypothesis hb : b ∈ S694hypothesis distinct : a ≠ b695hypothesis hr : r ∈ derangements(S ∖ {a})696697theorem throughLift.injective698  shows InjectiveBetween(throughLift(S, a, b, r), S ∖ {a}, S)699proof700  have subset := difference.subset_left at S, {a}701  have rInjective := Bijective.injective with702    (permutations.bijective with (derangements.permutation with hr))703  have tauInjective := Bijective.injective with704    (transposition.bijective at S, a, b with ha, hb)705  have tauRest := restrict.injective with tauInjective, subset706  unfold throughLift707  exact compose.injective with rInjective, tauRest708709theorem throughLift.apply (x : Set)710  requires hx : x ∈ S ∖ {a}711  shows throughLift(S, a, b, r)(x) = transposition(S, a, b)(r(x))712proof713  have subset := difference.subset_left at S, {a}714  have rFunction := derangements.function with hr715  have tauFunction := transposition.function at S, a, b with ha, hb716  have tauRest := restrict.domain_function with tauFunction, subset717  have rxIn := derangements.apply_closed with hr, hx718  have step := compose.apply with rFunction, tauRest, hx719  have inner := restrict.domain_apply with tauFunction, subset, rxIn720  simp [throughLift]721722theorem throughLift.avoids723  shows InjectiveBetween(throughLift(S, a, b, r), S ∖ {a}, S ∖ {b})724proof725  have injective := throughLift.injective at S, a, b, r with *726  have tauA := transposition.first at S, a, b with ha, hb727  have absent : ¬b ∈ functionImage(throughLift(S, a, b, r), S ∖ {a}, S)728    intro inside729    obtain ⟨bIn, x, hx, shape⟩ := functionImage.membership.forward with inside730    have value := throughLift.apply at S, a, b, r, x with *731    rw value at shape732    have rxIn := derangements.apply_closed with hr, hx733    have parts := difference.singleton_membership.forward with rxIn734    have equal : transposition(S, a, b)(r(x)) = transposition(S, a, b)(a)735      rw [← shape, tauA]736      rfl737    have rxA := transposition.apply_cancel with ha, hb, parts.left, ha, equal738    exact parts.right with rxA739  exact Injective.avoid with injective, absent740741theorem throughExtend.injective742  shows InjectiveBetween(throughExtend(S, a, b, r), S, S)743proof744  have narrowed := throughLift.avoids at S, a, b, r with *745  have aOut : ¬a ∈ S ∖ {a} by simp [difference.membership, singleton.membership]746  have bOut : ¬b ∈ S ∖ {b} by simp [difference.membership, singleton.membership]747  have extended := adjoinMap.injective with narrowed, aOut, bOut748  have domain := insert.restore with ha749  have codomain := insert.restore with hb750  rw [domain, codomain] at extended751  unfold throughExtend752  exact extended753754theorem throughExtend.apply_first755  shows throughExtend(S, a, b, r)(a) = b756proof757  have liftFunction := Injective.function with758    (throughLift.injective at S, a, b, r with *)759  have aOut : ¬a ∈ S ∖ {a} by simp [difference.membership, singleton.membership]760  unfold throughExtend761  exact adjoinMap.apply_new at throughLift(S, a, b, r), S ∖ {a}, S, a, b with762    liftFunction, aOut763764theorem throughExtend.apply_rest (x : Set)765  requires hx : x ∈ S ∖ {a}766  shows throughExtend(S, a, b, r)(x) = transposition(S, a, b)(r(x))767proof768  have liftFunction := Injective.function with769    (throughLift.injective at S, a, b, r with *)770  have aOut : ¬a ∈ S ∖ {a} by simp [difference.membership, singleton.membership]771  have outer : throughExtend(S, a, b, r)(x) = throughLift(S, a, b, r)(x)772    unfold throughExtend773    exact adjoinMap.apply_old at throughLift(S, a, b, r), S ∖ {a}, S,774      a, b, x with liftFunction, aOut, hx775  have inner := throughLift.apply at S, a, b, r, x with *776  rw [outer, inner]777  rfl778779theorem throughExtend.member780  shows throughExtend(S, a, b, r) ∈ throughFiber(S, a, b)781proof782  have injective := throughExtend.injective at S, a, b, r with *783  have atA := throughExtend.apply_first at S, a, b, r with *784  have tauB := transposition.second at S, a, b with ha, hb785  have ba : b ≠ a786    intro same787    apply distinct788    symm789    exact same790  have bInRest : b ∈ S ∖ {a} :=791    difference.singleton_membership.backward with ⟨hb, ba⟩792  have moves : ∀ x ∈ S, throughExtend(S, a, b, r)(x) ≠ x793    intros x hx794    have alternatives : x = a ∨ x ≠ a by tauto795    cases alternatives with isA | notA796    . rw [isA, atA]797      exact ba798    . have inRest : x ∈ S ∖ {a} :=799        difference.singleton_membership.backward with ⟨hx, notA⟩800      have value := throughExtend.apply_rest at S, a, b, r, x with *801      rw value802      have rxIn := derangements.apply_closed with hr, inRest803      have rxParts := difference.singleton_membership.forward with rxIn804      intro same805      have split : r(x) = b ∨ r(x) ≠ b by tauto806      cases split with isB | notB807      . rw [isB, tauB] at same808        apply notA809        symm810        exact same811      . have fixed := transposition.other at S, a, b, r(x) with812          ha, hb, rxParts.left, rxParts.right, notB813        rw fixed at same814        exact derangements.moves with hr, inRest, same815  have deranged := derangements.of_injective with finite, injective, moves816  have atB : throughExtend(S, a, b, r)(b) ≠ a817    have value := throughExtend.apply_rest at S, a, b, r, b with *818    rw value819    intro same820    have equal : transposition(S, a, b)(r(b)) = transposition(S, a, b)(b)821      rw [same, tauB]822      rfl823    have rbIn := derangements.apply_closed with hr, bInRest824    have rbParts := difference.singleton_membership.forward with rbIn825    have rbB := transposition.apply_cancel with ha, hb, rbParts.left, hb, equal826    exact derangements.moves with hr, bInRest, rbB827  exact throughFiber.membership.backward with ⟨deranged, atA, atB⟩828829end ThroughExtension830831theorem throughRestrict.surjective (S a b : Set)832  requires finite : Finite(S)833  requires ha : a ∈ S834  requires hb : b ∈ S835  requires distinct : a ≠ b836  shows SurjectiveBetween(throughRestrict(S, a, b), throughFiber(S, a, b),837    derangements(S ∖ {a}))838proof839  have graph := throughRestrict.function at S, a, b with finite, ha, hb840  have subset := difference.subset_left at S, {a}841  have involution := transposition.involution at S, a, b with ha, hb842  unfold SurjectiveBetween843  refine ⟨graph, ?_⟩844  intros r hr845  have inFiber := throughExtend.member at S, a, b, r with *846  refine ⟨throughExtend(S, a, b, r), inFiber, ?_⟩847  have value := throughRestrict.value at S, a, b, throughExtend(S, a, b, r)848    with finite, ha, hb, inFiber849  have restored : throughMap(S, a, b, throughExtend(S, a, b, r)) = r850    have pFunction := Injective.function with851      (throughExtend.injective at S, a, b, r with *)852    have inImage := throughRestrict.closed at S, a, b, throughExtend(S, a, b, r)853      with finite, ha, hb, inFiber854    have mapped := derangements.function at S ∖ {a},855      throughMap(S, a, b, throughExtend(S, a, b, r)) with inImage856    have rFunction := derangements.function at S ∖ {a}, r with hr857    apply FunctionBetween.ext with mapped, rFunction858    intros x hx859    have step := throughMap.apply with ha, hb, pFunction, hx860    have inner := throughExtend.apply_rest at S, a, b, r, x with *861    rw [step, inner]862    have rxIn := derangements.apply_closed with hr, hx863    exact InvolutionOn.apply with involution, (subset with r(x), rxIn)864  have related := FunctionBetween.relates_apply with graph, inFiber865  rw [value, restored] at related866  exact related867868theorem throughFiber.count (S a b : Set)869  requires finite : Finite(S)870  requires ha : a ∈ S871  requires hb : b ∈ S872  requires distinct : a ≠ b873  shows cardinality(throughFiber(S, a, b)) = cardinality(derangements(S ∖ {a}))874proof875  have injective := throughRestrict.injective with finite, ha, hb876  have surjective := throughRestrict.surjective with finite, ha, hb, distinct877  have finiteFiber := Finite.subset with (derangements.finite with finite),878    (throughFiber.subset at S, a, b)879  have bijective : BijectiveBetween(throughRestrict(S, a, b),880    throughFiber(S, a, b), derangements(S ∖ {a})) := ⟨injective, surjective⟩881  exact cardinality.bijective with finiteFiber, bijective882883-- The derangements sending a to b number d(S ∖ {a, b}) + d(S ∖ {a}).884theorem valueAt.fiber_count (S a b : Set)885  requires finite : Finite(S)886  requires ha : a ∈ S887  requires hb : b ∈ S888  requires distinct : a ≠ b889  shows cardinality(functionPreimage(valueAt(S, a), derangements(S), {b})) =890    cardinality(derangements((S ∖ {a}) ∖ {b})) +891    cardinality(derangements(S ∖ {a}))892proof893  have preimage := valueAt.preimage at S, a, b with ha894  have finiteAll := derangements.finite with finite895  have finiteSwap := Finite.subset with finiteAll, (swapFiber.subset at S, a, b)896  have finiteThrough := Finite.subset with finiteAll,897    (throughFiber.subset at S, a, b)898  have split := cardinality.union_disjoint with finiteSwap, finiteThrough,899    (swapFiber.disjoint at S, a, b)900  have swapCount := swapFiber.count with finite, ha, hb, distinct901  have throughCount := throughFiber.count with finite, ha, hb, distinct902  rw [preimage, split, swapCount, throughCount]903  rfl904905-- The recurrence: with |S| = n + 2, every b ∈ S ∖ {a} receives a from906-- d(n) + d(n + 1) derangements.907theorem derangements.count_pair (n : Nat)908  shows ∀ S,909    (HasCardinality(S, n) → cardinality(derangements(S)) = derangement(n)) ∧910    (HasCardinality(S, n + 1) →911      cardinality(derangements(S)) = derangement(n + 1))912proof913  induction n914  | zero =>915    intro S916    constructor917    . intro counted918      have empty := HasCardinality.empty_of_zero at S with counted919      rw [empty, derangements.empty_count, derangement.zero]920      rfl921    . intro counted922      have one : 0 + 1 = 1 by compute923      rw one at counted924      have finite := Finite.from_cardinality with counted925      have size := cardinality.eq_of_has with counted926      have iff := cardinality.one_iff with finite927      obtain ⟨x, shape⟩ := iff.forward with size928      rw [one, shape, derangements.singleton_count, derangement.one]929      rfl930  | k + 1 using ih =>931    intro S932    constructor933    . intro counted934      have parts := ih with S935      exact parts.right with counted936    . intro counted937      have two : k + 1 + 1 = succ(succ(k)) by ring938      rw two at counted939      have finite := Finite.from_cardinality with counted940      obtain ⟨a, ha⟩ := HasCardinality.exists_member with counted941      have rest := HasCardinality.remove with counted, ha942      have restFinite := Finite.from_cardinality with rest943      have restSize := cardinality.eq_of_has with rest944      have restSubset := difference.subset_left at S, {a}945      have restParts := ih with S ∖ {a}946      have one : k + 1 = succ(k) := add.right_one with *947      have restPlus : HasCardinality(S ∖ {a}, k + 1)948        rw one949        exact rest950      have restCount := restParts.right with restPlus951      have finiteAll := derangements.finite with finite952      have graph := valueAt.function at S, a with ha953      have total := cardinality.sum_of_preimages with954        graph, finiteAll, restFinite955      have natK := derangement.natural at k956      have natK1 := derangement.natural at k + 1957      have agree : ∀ b ∈ S ∖ {a},958          preimageSize(valueAt(S, a), derangements(S), S ∖ {a})(b) =959          derangement(k) + derangement(k + 1)960        intros b hb961        obtain ⟨bInS, ba⟩ := difference.singleton_membership.forward with hb962        have ab : a ≠ b963          intro same964          apply ba965          symm966          exact same967        have value := preimageSize.value at968          valueAt(S, a), derangements(S), S ∖ {a}, b with finiteAll, hb969        have fiberCount := valueAt.fiber_count with finite, ha, bInS, ab970        rw [value, fiberCount, restCount]971        have smaller := HasCardinality.remove with rest, hb972        have smallerParts := ih with (S ∖ {a}) ∖ {b}973        have rewrite := smallerParts.left with smaller974        rw rewrite975        rfl976      have sum := natSum.constant with restFinite, agree977      rw [total, sum, restSize]978      have shape : succ(k) * (derangement(k) + derangement(k + 1)) =979          (k + 1) * (derangement(k + 1) + derangement(k))980        rw ← one981        ring982      have twoPlus : k + 1 + 1 = k + 2 by ring983      rw [shape, twoPlus, derangement.recurrence]984      rfl985986theorem derangements.count (S : Set)987  requires finite : Finite(S)988  shows cardinality(derangements(S)) = derangement(cardinality(S))989proof990  have natS := cardinality.nat with finite991  have parts := derangements.count_pair at cardinality(S) with S992  exact parts.left with (cardinality.correct with finite)993994-- The number of derangements of n points.995theorem derangements.natural_count (n : Nat)996  shows cardinality(derangements(n)) = derangement(n)997proof998  have count := derangements.count with (Finite.natural at n)999  rw [count, cardinality.natural]1000  rfl10011002theorem derangements.recurrence (n : Nat)1003  shows cardinality(derangements(n + 2)) =1004    (n + 1) * (cardinality(derangements(n + 1)) + cardinality(derangements(n)))1005proof1006  rw [derangements.natural_count, derangements.natural_count,1007    derangements.natural_count]1008  exact derangement.recurrence at n10091010-- The derangement formula for the count itself.1011theorem derangements.formula (n : Nat)1012  shows integerOfNat(cardinality(derangements(n))) = derangementSum(n, n + 1)1013proof1014  rw derangements.natural_count1015  exact derangement.closed_form at n1016