Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Mathlib.Data.Finset.Sort public import Mathlib.Data.Fintype.Pi public import Mathlib.Data.Fintype.Prod public import Mathlib.Data.Nat.Factorial.DoubleFactorial

Fin involutions

Some properties of involutions of Fin n.

These involutions are used in e.g. proving results about Wick contractions.

@[expose] public section

There is an equivalence between involutions of Fin n.succ and involutions of Fin n and an optional valid choice of an element in Fin n (which is where 0 in Fin n.succ will be sent).

n:ℕf✝:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f:Fin n → Fin nhf:Function.Involutive ff0:Option (Fin n)hf0:∀ (h : f0.isSome = true), ↑⟨f, hf⟩ (f0.get h) = f0.get hi:Fin nhs:f0.isSome = truehx:¬(f0.get hs).succ = 0⊢ f0.get ⋯ = i ↔ ∃ (h : f0.isSome = true), f0.get h = i All goals completed! 🐙 n:ℕf✝:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f:Fin n → Fin nhf:Function.Involutive ff0:Option (Fin n)hf0:∀ (h : f0.isSome = true), ↑⟨f, hf⟩ (f0.get h) = f0.get hi:Fin nhs:¬f0.isSome = true⊢ (∃ (h : ¬(if h : f0.isSome = true then Fin.cons (f0.get ⋯).succ (Function.update (Fin.succ ∘ f) (f0.get ⋯) 0) else Fin.cons 0 (Fin.succ ∘ f)) 0 = 0), ((if h : f0.isSome = true then Fin.cons (f0.get ⋯).succ (Function.update (Fin.succ ∘ f) (f0.get ⋯) 0) else Fin.cons 0 (Fin.succ ∘ f)) 0).pred ⋯ = i) ↔ f0 = some i n:ℕf✝:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f:Fin n → Fin nhf:Function.Involutive ff0:Option (Fin n)hf0:∀ (h : f0.isSome = true), ↑⟨f, hf⟩ (f0.get h) = f0.get hi:Fin nhs:¬f0.isSome = true⊢ ¬f0 = some i n:ℕf✝:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f:Fin n → Fin nhf:Function.Involutive ff0:Option (Fin n)hf0:∀ (h : f0.isSome = true), ↑⟨f, hf⟩ (f0.get h) = f0.get hi:Fin nhs:f0 = none⊢ ¬f0 = some i n:ℕf✝:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f:Fin n → Fin nhf:Function.Involutive fi:Fin nhf0:∀ (h : none.isSome = true), ↑⟨f, hf⟩ (none.get h) = none.get h⊢ ¬none = some i All goals completed! 🐙
n:ℕf1:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f2:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }h1:f1.fst = f2.fst⊢ ∀ (x : Option (Fin n)), (∀ (h : x.isSome = true), ↑f2.fst (x.get h) = x.get h) ↔ ∀ (h : x.isSome = true), ↑f2.fst (x.get h) = x.get h; All goals completed! 🐙) f2.2) : f1 = f2 := n:ℕf1:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }f2:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }h1:f1.fst = f2.fsth2:f1.snd = (Equiv.subtypeEquivRight ⋯) f2.snd⊢ f1 = f2 n:ℕf2:(f : { f // Function.Involutive f }) × { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }fst✝:{ f // Function.Involutive f }snd✝:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }h1:⟨fst✝, snd✝⟩.fst = f2.fsth2:⟨fst✝, snd✝⟩.snd = (Equiv.subtypeEquivRight ⋯) f2.snd⊢ ⟨fst✝, snd✝⟩ = f2 n:ℕfst✝¹:{ f // Function.Involutive f }snd✝¹:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }fst✝:{ f // Function.Involutive f }snd✝:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }h1:⟨fst✝¹, snd✝¹⟩.fst = ⟨fst✝, snd✝⟩.fsth2:⟨fst✝¹, snd✝¹⟩.snd = (Equiv.subtypeEquivRight ⋯) ⟨fst✝, snd✝⟩.snd⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩ n:ℕfst✝¹:{ f // Function.Involutive f }snd✝¹:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }fst✝:{ f // Function.Involutive f }snd✝:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }h1:fst✝¹ = fst✝h2:snd✝¹ = (Equiv.subtypeEquivRight ⋯) snd✝⊢ ⟨fst✝¹, snd✝¹⟩ = ⟨fst✝, snd✝⟩ n:ℕfst✝:{ f // Function.Involutive f }snd✝¹:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }snd✝:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }h2:snd✝¹ = (Equiv.subtypeEquivRight ⋯) snd✝⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩ n:ℕfst:{ f // Function.Involutive f }snd:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }snd_1:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }h2:snd✝¹ = (Equiv.subtypeEquivRight ⋯) snd✝⊢ ⟨fst✝, snd✝¹⟩ = ⟨fst✝, snd✝⟩ n:ℕfst:{ f // Function.Involutive f }snd:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }snd_1:{ i // ∀ (h : i.isSome = true), ↑fst✝ (i.get h) = i.get h }h2:snd✝¹ = (Equiv.subtypeEquivRight ⋯) snd✝⊢ (Equiv.subtypeEquivRight ⋯) snd_1 = snd_1 n:ℕval:Fin n → Fin nproperty:Function.Involutive valsnd:{ i // ∀ (h : i.isSome = true), ↑⟨val, property⟩ (i.get h) = i.get h }snd_1:{ i // ∀ (h : i.isSome = true), ↑⟨val, property⟩ (i.get h) = i.get h }h2:snd = (Equiv.subtypeEquivRight ⋯) snd_1⊢ (Equiv.subtypeEquivRight ⋯) snd_1 = snd_1 n:ℕval:Fin n → Fin nproperty:Function.Involutive valsnd_1:{ i // ∀ (h : i.isSome = true), ↑⟨val, property⟩ (i.get h) = i.get h }val_1:Option (Fin n)property_1:∀ (h : val_1.isSome = true), ↑⟨val, property⟩ (val_1.get h) = val_1.get hh2:⟨val_1, property_1⟩ = (Equiv.subtypeEquivRight ⋯) snd_1⊢ (Equiv.subtypeEquivRight ⋯) snd_1 = snd_1 n:ℕval:Fin n → Fin nproperty:Function.Involutive valval_1:Option (Fin n)property_1:∀ (h : val_1.isSome = true), ↑⟨val, property⟩ (val_1.get h) = val_1.get hval_2:Option (Fin n)property_2:∀ (h : val_2.isSome = true), ↑⟨val, property⟩ (val_2.get h) = val_2.get hh2:⟨val_1, property_1⟩ = (Equiv.subtypeEquivRight ⋯) ⟨val_2, property_2⟩⊢ (Equiv.subtypeEquivRight ⋯) ⟨val_2, property_2⟩ = ⟨val_2, property_2⟩ n:ℕval:Fin n → Fin nproperty:Function.Involutive valval_1:Option (Fin n)property_1:∀ (h : val_1.isSome = true), ↑⟨val, property⟩ (val_1.get h) = val_1.get hval_2:Option (Fin n)property_2:∀ (h : val_2.isSome = true), ↑⟨val, property⟩ (val_2.get h) = val_2.get hh2:⟨val_1, property_1⟩ = (Equiv.subtypeEquivRight ⋯) ⟨val_2, property_2⟩⊢ (Equiv.subtypeEquivRight ⋯) ⟨val_2, property_2⟩ = ⟨val_2, property_2⟩ All goals completed! 🐙

Given an involution of Fin n, the optional choice of an element in Fin n which maps to itself is equivalent to the optional choice of an element in Fin (Finset.univ.filter fun i => f.1 i = i).card.

n:ℕf:{ f // Function.Involutive f }e1:{ i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option { i // ↑f i = i } := { toFun := fun i => match i with | ⟨some i, h⟩ => some ⟨i, ⋯⟩ | ⟨none, h⟩ => none, invFun := fun i => match i with | some ⟨i, h⟩ => ⟨some i, ⋯⟩ | none => ⟨none, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }s:Finset (Fin n) := {i | ↑f i = i}e2':{ i // ↑f i = i } ≃ ↥s := Equiv.subtypeEquivProp ⋯e2:↥s ≃ Fin s.card := (s.orderIsoOfFin ⋯).symm.toEquiv⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) All goals completed! 🐙
lemma involutionAddEquiv_none_image_zero {n : ℕ} : {f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}} → involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none → f.1 ⟨0, Nat.zero_lt_succ n⟩ = ⟨0, Nat.zero_lt_succ n⟩ := n:ℕ⊢ ∀ {f : { f // Function.Involutive f }}, (involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none → ↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩ n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none⊢ ↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩ n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonehf0:¬↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩⊢ False n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonehf0:¬↑f 0 = 0⊢ False n:ℕf:{ f // Function.Involutive f }hf0:¬↑f 0 = 0h:({ toFun := fun i => match i with | ⟨some i, h⟩ => some ⟨i, ⋯⟩ | ⟨none, h⟩ => none, invFun := fun i => match i with | some ⟨i, h⟩ => ⟨some i, ⋯⟩ | none => ⟨none, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.trans ((Equiv.subtypeEquivProp ⋯).trans ({i | (if h : ↑f i.succ = 0 then i else (↑f i.succ).pred h) = i}.orderIsoOfFin ⋯).symm.toEquiv).optionCongr) ⟨some ((↑f 0).pred hf0), ⋯⟩ = none⊢ False All goals completed! 🐙n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 = (Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (Equiv.refl (Option (Fin {i | ↑f1 i = i}.card)))) All goals completed! 🐙lemma involutionAddEquiv_cast' {m : ℕ} {f1 f2 : {f : Fin m → Fin m // Function.Involutive f}} {N : ℕ} (hf : f1 = f2) (n : Option (Fin N)) (hn1 : N = (Finset.filter (fun i => f1.1 i = i) Finset.univ).card) (hn2 : N = (Finset.filter (fun i => f2.1 i = i) Finset.univ).card) : HEq ((involutionAddEquiv f1).symm (Option.map (finCongr hn1) n)) ((involutionAddEquiv f2).symm (Option.map (finCongr hn2) n)) := m:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }N:ℕhf:f1 = f2n:Option (Fin N)hn1:N = {i | ↑f1 i = i}.cardhn2:N = {i | ↑f2 i = i}.card⊢ (involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn1)) n) ≍ (involutionAddEquiv f2).symm (Option.map (⇑(finCongr hn2)) n) m:ℕf1:{ f // Function.Involutive f }N:ℕn:Option (Fin N)hn1:N = {i | ↑f1 i = i}.cardhn2:N = {i | ↑f1 i = i}.card⊢ (involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn1)) n) ≍ (involutionAddEquiv f1).symm (Option.map (⇑(finCongr hn2)) n) All goals completed! 🐙lemma involutionAddEquiv_none_succ {n : ℕ} {f : {f : Fin n.succ → Fin n.succ // Function.Involutive f}} (h : involutionAddEquiv (involutionCons n f).1 (involutionCons n f).2 = none) (x : Fin n) : f.1 x.succ = x.succ ↔ (involutionCons n f).1.1 x = x := n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin n⊢ ↑f x.succ = x.succ ↔ ↑((involutionCons n) f).fst x = x n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin n⊢ ↑f x.succ = x.succ ↔ ∀ (h : ¬↑f x.succ = 0), (↑f x.succ).pred h = x n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin nhx:¬↑f x.succ = ⟨0, ⋯⟩⊢ ↑f x.succ = x.succ ↔ ∀ (h : ¬↑f x.succ = 0), (↑f x.succ).pred h = x exact Iff.intro (fun h2 ↦ n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonex:Fin nhx:¬↑f x.succ = ⟨0, ⋯⟩h2:↑f x.succ = x.succ⊢ ∀ (h : ¬↑f x.succ = 0), (↑f x.succ).pred h = x All goals completed! 🐙) (fun h2 ↦ (Fin.pred_eq_iff_eq_succ hx).mp (h2 hx))

Equivalences of involutions with no fixed points.

The main aim of these equivalences is to define involutionNoFixedZeroEquivProd.

Fixed point free involutions of Fin n.succ can be separated based on where they sent 0.

def involutionNoFixedEquivSum {n : ℕ} : {f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ ∀ i, f i ≠ i} ≃ Σ (k : Fin n), {f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} where toFun f := ⟨(f.1 0).pred (f.2.2 0), ⟨f.1, f.2.1, n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n.succ), f i ≠ i }⊢ (∀ (i : Fin n.succ), ↑f i ≠ i) ∧ ↑f 0 = ((↑f 0).pred ⋯).succ All goals completed! 🐙⟩⟩ invFun f := ⟨f.2.1, ⟨f.2.2.1, f.2.2.2.1⟩⟩ left_inv f := rfl right_inv f := n:ℕf:(k : Fin n) × { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }⊢ (fun f => ⟨(↑f 0).pred ⋯, ⟨↑f, ⋯⟩⟩) ((fun f => ⟨↑f.snd, ⋯⟩) f) = f n:ℕf:(k : Fin n) × { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }⊢ ↑((fun f => ⟨(↑f 0).pred ⋯, ⟨↑f, ⋯⟩⟩) ((fun f => ⟨↑f.snd, ⋯⟩) f)).fst = ↑f.fstn:ℕf:(k : Fin n) × { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }x✝:Fin n.succ⊢ ↑(↑((fun f => ⟨(↑f 0).pred ⋯, ⟨↑f, ⋯⟩⟩) ((fun f => ⟨↑f.snd, ⋯⟩) f)).snd x✝) = ↑(↑f.snd x✝) n:ℕf:(k : Fin n) × { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }⊢ ↑((fun f => ⟨(↑f 0).pred ⋯, ⟨↑f, ⋯⟩⟩) ((fun f => ⟨↑f.snd, ⋯⟩) f)).fst = ↑f.fstn:ℕf:(k : Fin n) × { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }x✝:Fin n.succ⊢ ↑(↑((fun f => ⟨(↑f 0).pred ⋯, ⟨↑f, ⋯⟩⟩) ((fun f => ⟨↑f.snd, ⋯⟩) f)).snd x✝) = ↑(↑f.snd x✝) try All goals completed! 🐙

The condition on fixed point free involutions of Fin n.succ for a fixed value of f 0, can be modified by conjugation with an equivalence.

All goals completed! 🐙, n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }⊢ ∀ (i : Fin n.succ), (⇑e.symm ∘ (⇑e ∘ ↑f ∘ ⇑e.symm) ∘ ⇑e) i ≠ i All goals completed! 🐙, n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }⊢ (⇑e.symm ∘ (⇑e ∘ ↑f ∘ ⇑e.symm) ∘ ⇑e) 0 = k.succ All goals completed! 🐙⟩ invFun f := ⟨e.symm ∘ f.1 ∘ e, n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }⊢ Function.Involutive (⇑e.symm ∘ ↑f ∘ ⇑e) n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }i:Fin n.succ⊢ (⇑e.symm ∘ ↑f ∘ ⇑e) ((⇑e.symm ∘ ↑f ∘ ⇑e) i) = i All goals completed! 🐙, n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }⊢ ∀ (i : Fin n.succ), (⇑e.symm ∘ ↑f ∘ ⇑e) i ≠ i All goals completed! 🐙, n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }⊢ (⇑e.symm ∘ ↑f ∘ ⇑e) 0 = k.succ All goals completed! 🐙⟩ left_inv f := n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }⊢ (fun f => ⟨⇑e.symm ∘ ↑f ∘ ⇑e, ⋯⟩) ((fun f => ⟨⇑e ∘ ↑f ∘ ⇑e.symm, ⋯⟩) f) = f n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f 0 = k.succ }i:Fin n.succ⊢ ↑(↑((fun f => ⟨⇑e.symm ∘ ↑f ∘ ⇑e, ⋯⟩) ((fun f => ⟨⇑e ∘ ↑f ∘ ⇑e.symm, ⋯⟩) f)) i) = ↑(↑f i); All goals completed! 🐙 right_inv f := n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }⊢ (fun f => ⟨⇑e ∘ ↑f ∘ ⇑e.symm, ⋯⟩) ((fun f => ⟨⇑e.symm ∘ ↑f ∘ ⇑e, ⋯⟩) f) = f n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:{ f // Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }i:Fin n.succ⊢ ↑(↑((fun f => ⟨⇑e ∘ ↑f ∘ ⇑e.symm, ⋯⟩) ((fun f => ⟨⇑e.symm ∘ ↑f ∘ ⇑e, ⋯⟩) f)) i) = ↑(↑f i); All goals completed! 🐙

The condition on fixed point free involutions of Fin n.succ for a fixed value of f 0 given an equivalence e, can be modified so that only the condition on f 0 is up-to the equivalence e.

n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive f⊢ Function.Involutive f ∧ (∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ ↔ Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive f⊢ Function.Involutive f → e.symm (f (e 0)) = k.succ → ((∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) ↔ ∀ (i : Fin (n + 1)), ¬f i = i) n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ⊢ (∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) ↔ ∀ (i : Fin (n + 1)), ¬f i = i n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ⊢ (∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) → ∀ (i : Fin (n + 1)), ¬f i = in:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ⊢ (∀ (i : Fin (n + 1)), ¬f i = i) → ∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ⊢ (∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i) → ∀ (i : Fin (n + 1)), ¬f i = i n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh:∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = ii:Fin (n + 1)⊢ ¬f i = i All goals completed! 🐙 n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succ⊢ (∀ (i : Fin (n + 1)), ¬f i = i) → ∀ (i : Fin (n + 1)), ¬e.symm (f (e i)) = i n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh:∀ (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)⊢ ¬e.symm (f (e i)) = i n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh:∀ (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)hi:¬f (e i) = e i⊢ ¬e.symm (f (e i)) = i n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh:∀ (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)hi:¬f (e i) = e ihn:e.symm (f (e i)) = i⊢ False n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh1✝:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive fh1:Function.Involutive fh2:e.symm (f (e 0)) = k.succh:∀ (i : Fin (n + 1)), ¬f i = ii:Fin (n + 1)hi:¬f (e i) = e (e.symm (f (e i)))hn:e.symm (f (e i)) = i⊢ False All goals completed! 🐙

Fixed point free involutions of Fin n.succ fixing (e.symm ∘ f ∘ e) = k.succ for a given e are equivalent to fixing f (e 0) = e k.succ.

def involutionNoFixedZeroSetEquivEquiv' {n : ℕ} (k : Fin n) (e : Fin n.succ ≃ Fin n.succ) : {f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} ≃ {f : Fin n.succ → Fin n.succ // Function.Involutive f ∧ (∀ i, f i ≠ i) ∧ f (e 0) = e k.succ} := n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succ⊢ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ } ≃ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ f (e 0) = e k.succ } n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succ⊢ ∀ (x : Fin n.succ → Fin n.succ), Function.Involutive x ∧ (∀ (i : Fin n.succ), x i ≠ i) ∧ (⇑e.symm ∘ x ∘ ⇑e) 0 = k.succ ↔ Function.Involutive x ∧ (∀ (i : Fin n.succ), x i ≠ i) ∧ x (e 0) = e k.succ n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succ⊢ ∀ (x : Fin (n + 1) → Fin (n + 1)), Function.Involutive x → (∀ (i : Fin (n + 1)), ¬x i = i) → (e.symm (x (e 0)) = k.succ ↔ x (e 0) = e k.succ) n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin (n + 1) → Fin (n + 1)hi:Function.Involutive fh1:∀ (i : Fin (n + 1)), ¬f i = i⊢ e.symm (f (e 0)) = k.succ ↔ f (e 0) = e k.succ All goals completed! 🐙

Fixed point involutions of Fin n.succ.succ with f 0 = k.succ are equivalent to fixed point involutions with f 0 = 1.

n:ℕk:Fin n.succf:Fin (n + 1 + 1) → Fin (n + 1 + 1)hi:Function.Involutive fh1:∀ (i : Fin (n + 1 + 1)), ¬f i = i⊢ 0 ≠ k.succn:ℕk:Fin n.succf:Fin (n + 1 + 1) → Fin (n + 1 + 1)hi:Function.Involutive fh1:∀ (i : Fin (n + 1 + 1)), ¬f i = i⊢ 0 ≠ 1 n:ℕk:Fin n.succf:Fin (n + 1 + 1) → Fin (n + 1 + 1)hi:Function.Involutive fh1:∀ (i : Fin (n + 1 + 1)), ¬f i = i⊢ 0 ≠ k.succ All goals completed! 🐙 n:ℕk:Fin n.succf:Fin (n + 1 + 1) → Fin (n + 1 + 1)hi:Function.Involutive fh1:∀ (i : Fin (n + 1 + 1)), ¬f i = i⊢ 0 ≠ 1 All goals completed! 🐙

Fixed point involutions of Fin n.succ.succ fixing f 0 = 1 are equivalent to fixed point involutions of Fin n.

n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0⊢ (fun f => let f' := fun i => match i with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ; ⟨f', ⋯⟩) ((fun f => have f_succ_succ_ne_zero_one := ⋯; let f' := ↑f ∘ Fin.succ ∘ Fin.succ; have hf' := ⋯; let f'' := fun i => (f' i).pred ⋯; have hf'' := ⋯; let f''' := fun i => (f'' i).pred ⋯; ⟨f''', ⋯⟩) f) = f n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0⊢ ⟨fun i => match i with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => ↑f ⟨n_1 + 1 + 1, ⋯⟩, ⋯⟩ = f n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i:Fin (n + 1 + 1)⊢ ↑(↑⟨fun i => match i with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => ↑f ⟨n_1 + 1 + 1, ⋯⟩, ⋯⟩ i) = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i:Fin (n + 1 + 1)⊢ ↑(match i with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => ↑f ⟨n_1 + 1 + 1, ⋯⟩) = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i✝:Fin n✝.succ.succh✝:0 < n.succ.succ⊢ ↑1 = ↑(↑f ⟨0, h✝⟩)n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i✝:Fin n✝.succ.succh✝:1 < n.succ.succ⊢ ↑0 = ↑(↑f ⟨1, h✝⟩)n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succ⊢ ↑(↑f ⟨n✝ + 1 + 1, ⋯⟩) = ↑(↑f ⟨n✝.succ.succ, h✝⟩) n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i✝:Fin n✝.succ.succh✝:0 < n.succ.succ⊢ ↑1 = ↑(↑f ⟨0, h✝⟩) All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i✝:Fin n✝.succ.succh✝:1 < n.succ.succ⊢ ↑0 = ↑(↑f ⟨1, h✝⟩) All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }hf1:↑f 1 = 0i✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succ⊢ ↑(↑f ⟨n✝ + 1 + 1, ⋯⟩) = ↑(↑f ⟨n✝.succ.succ, h✝⟩) All goals completed! 🐙 right_inv f := n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ (fun f => have f_succ_succ_ne_zero_one := ⋯; let f' := ↑f ∘ Fin.succ ∘ Fin.succ; have hf' := ⋯; let f'' := fun i => (f' i).pred ⋯; have hf'' := ⋯; let f''' := fun i => (f'' i).pred ⋯; ⟨f''', ⋯⟩) ((fun f => let f' := fun i => match i with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ; ⟨f', ⋯⟩) f) = f n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ ⟨fun i => ((match i.succ.succ with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ).pred ⋯).pred ⋯, ⋯⟩ = f n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin n⊢ ↑(↑⟨fun i => ((match i.succ.succ with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ).pred ⋯).pred ⋯, ⋯⟩ i) = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin n⊢ ↑(match i.succ.succ with | ⟨0, h⟩ => 1 | ⟨1, h⟩ => 0 | ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ) - 1 - 1 = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:i.succ.succ = ⟨0, h✝⟩⊢ ↑1 - 1 - 1 = ↑(↑f i)n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:i.succ.succ = ⟨1, h✝⟩⊢ ↑0 - 1 - 1 = ↑(↑f i)n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ ↑(↑f ⟨n✝, ⋯⟩).succ.succ - 1 - 1 = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:i.succ.succ = ⟨0, h✝⟩⊢ ↑1 - 1 - 1 = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succh✝:0 < n.succ.succh:i.succ.succ = ⟨0, h✝⟩⊢ ↑1 - 1 - 1 = ↑(↑f i) All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:i.succ.succ = ⟨1, h✝⟩⊢ ↑0 - 1 - 1 = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succh✝:1 < n.succ.succh:i.succ.succ = ⟨1, h✝⟩⊢ ↑0 - 1 - 1 = ↑(↑f i) All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ ↑(↑f ⟨n✝, ⋯⟩).succ.succ - 1 - 1 = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ ↑(↑f ⟨n✝, ⋯⟩) = ↑(↑f i) n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ ↑f ⟨n✝, ⋯⟩ = ↑f i n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin ni✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:i.succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ ⟨n✝, ⋯⟩ = i All goals completed! 🐙

Fixed point involutions of Fin n.succ.succ for fixed f 0 = k.succ are equivalent to fixed point involutions of Fin n.

def involutionNoFixedZeroSetEquiv {n : ℕ} (k : Fin n.succ) : {f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ i, f i ≠ i) ∧ f 0 = k.succ} ≃ {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} := (involutionNoFixedZeroSetEquivSetOne k).trans involutionNoFixedSetOne

The type of fixed point free involutions of Fin n.succ.succ is equivalent to the sum of Fin n.succ copies of fixed point involutions of Fin n.

def involutionNoFixedEquivSumSame {n : ℕ} : {f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ i, f i ≠ i)} ≃ Σ (_ : Fin n.succ), {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} := involutionNoFixedEquivSum.trans <| .sigmaCongrRight involutionNoFixedZeroSetEquiv

Ever fixed-point free involutions of Fin n.succ.succ can be decomposed into a element of Fin n.succ (where 0 is sent) and a fixed-point free involution of Fin n.

def involutionNoFixedZeroEquivProd {n : ℕ} : {f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ i, f i ≠ i)} ≃ Fin n.succ × {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} := involutionNoFixedEquivSumSame.trans <| .sigmaEquivProd ..

Cardinality

The type of fixed-point free involutions of Fin n is finite.

instance {n : ℕ} : Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } := n:ℕ⊢ Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } n:ℕthis:DecidablePred fun x => Function.Involutive x⊢ Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } All goals completed! 🐙
lemma involutionNoFixed_card_succ {n : ℕ} : Fintype.card {f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧ (∀ i, f i ≠ i)} = n.succ * Fintype.card {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} := n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n.succ.succ), f i ≠ i } = n.succ * Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } All goals completed! 🐙lemma involutionNoFixed_card_mul_two : (n : ℕ) → Fintype.card {f : Fin (2 * n) → Fin (2 * n) // Function.Involutive f ∧ (∀ i, f i ≠ i)} = (2 * n - 1)‼ | 0 => rfl n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ)), f i ≠ i } = (2 * n.succ - 1)‼ n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ)), f i ≠ i } = (2 * n.succ - 1)‼ erw [n:ℕ⊢ (Nat.mul 2 n).succ * Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (Nat.mul 2 n)), f i ≠ i } = (2 * n.succ - 1)‼ n:ℕ⊢ (Nat.mul 2 n).succ * (2 * n - 1)‼ = (2 * n.succ - 1)‼n:ℕ⊢ (Nat.mul 2 n).succ * (2 * n - 1)‼ = (2 * n.succ - 1)‼ All goals completed! 🐙lemma involutionNoFixed_card_mul_two_plus_one : (n : ℕ) → Fintype.card {f : Fin (2 * n + 1) → Fin (2 * n + 1) // Function.Involutive f ∧ (∀ i, f i ≠ i)} = 0 | 0 => rfl n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ + 1)), f i ≠ i } = 0 n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ + 1)), f i ≠ i } = 0 erw [n:ℕ⊢ (Nat.mul 2 n + 1).succ * Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (Nat.mul 2 n + 1)), f i ≠ i } = 0 n:ℕ⊢ (Nat.mul 2 n + 1).succ * 0 = 0n:ℕ⊢ (Nat.mul 2 n + 1).succ * 0 = 0 All goals completed! 🐙n:ℕr:ℕhr:n = r + rhr':n = 2 * r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼ r:ℕhr:2 * r = r + r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * r)), f i ≠ i } = (2 * r - 1)‼ All goals completed! 🐙lemma involutionNoFixed_card_odd : (n : ℕ) → (ho : Odd n) → Fintype.card {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} = 0 := ⊢ ∀ (n : ℕ), Odd n → Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0 n:ℕho:Odd n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0 n:ℕr:ℕhr:n = 2 * r + 1⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0 r:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * r + 1)), f i ≠ i } = 0 All goals completed! 🐙