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.DoubleFactorialFin 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).
pos 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
simp [hs] All goals completed! 🐙
· neg 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 simp only [hs, Bool.false_eq_true, ↓reduceDIte, Fin.cons_zero, not_true_eq_false,
IsEmpty.exists_iff, false_iff] neg 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
simp only [Bool.not_eq_true, Option.isSome_eq_false_iff, Option.isNone_iff_eq_none] at hs neg 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
subst hs neg 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
exact ne_of_beq_false rfl All goals completed! 🐙
lemma involutionCons_ext {n : ℕ} {f1 f2 : (f : {f : Fin n → Fin n // Function.Involutive f}) ×
{i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}}
(h1 : f1.1 = f2.1) (h2 : f1.2 = Equiv.subtypeEquivRight (by 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), ↑f1.fst (x.get h) = x.get h rw [h1 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 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] 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; simp All goals completed! 🐙) f2.2) : f1 = f2 := by 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
cases f1 mk 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
cases f2 mk.mk 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✝⟩
simp only at h1 h2 mk.mk 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✝⟩
subst h1 mk.mk 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✝⟩
rename_i fst snd snd_1 mk.mk 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✝⟩
simp_all only [Sigma.mk.inj_iff, heq_eq_eq, true_and] mk.mk 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
obtain ⟨val, property⟩ := fst mk.mk 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
obtain ⟨val_1, property_1⟩ := snd mk.mk 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
obtain ⟨val_2, property_2⟩ := snd_1 mk.mk 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⟩
simp_all only mk.mk 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⟩
rfl 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.
def involutionAddEquiv {n : ℕ} (f : {f : Fin n → Fin n // Function.Involutive f}) :
{i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)} ≃
Option (Fin (Finset.univ.filter fun i => f.1 i = i).card) := by n:ℕf:{ f // Function.Involutive f }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
let e1 : {i : Option (Fin n) // ∀ (h : i.isSome), f.1 (Option.get i h) = (Option.get i h)}
≃ Option {i : Fin n // f.1 i = i} :=
{ toFun := fun i => match i with
| ⟨some i, h⟩ => some ⟨i, by n:ℕf:{ f // Function.Involutive f }i✝:{ i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h }i:Fin nh:∀ (h : (some i).isSome = true), ↑f ((some i).get h) = (some i).get h⊢ ↑f i = i 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) simpa using h All goals completed! 🐙 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)⟩
| ⟨none, h⟩ => none
invFun := fun i => match i with
| some ⟨i, h⟩ => ⟨some i, by n:ℕf:{ f // Function.Involutive f }i✝:Option { i // ↑f i = i }i:Fin nh:↑f i = i⊢ ∀ (h : (some i).isSome = true), ↑f ((some i).get h) = (some i).get h 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) simpa using h All goals completed! 🐙 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)⟩
| none => ⟨none, by n:ℕf:{ f // Function.Involutive f }i:Option { i // ↑f i = i }⊢ ∀ (h : none.isSome = true), ↑f (none.get h) = none.get h 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) simp All goals completed! 🐙 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)⟩
left_inv := by n:ℕf:{ f // Function.Involutive f }⊢ Function.LeftInverse
(fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
rintro ⟨_ | i, h⟩ none n:ℕf:{ f // Function.Involutive f }h:∀ (h : none.isSome = true), ↑f (none.get h) = none.get h⊢ (fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
((fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
⟨none, h⟩) =
⟨none, h⟩some n:ℕf:{ f // Function.Involutive f }i:Fin nh:∀ (h : (some i).isSome = true), ↑f ((some i).get h) = (some i).get h⊢ (fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
((fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
⟨some i, h⟩) =
⟨some i, h⟩ 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) <;> none n:ℕf:{ f // Function.Involutive f }h:∀ (h : none.isSome = true), ↑f (none.get h) = none.get h⊢ (fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
((fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
⟨none, h⟩) =
⟨none, h⟩some n:ℕf:{ f // Function.Involutive f }i:Fin nh:∀ (h : (some i).isSome = true), ↑f ((some i).get h) = (some i).get h⊢ (fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
((fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
⟨some i, h⟩) =
⟨some i, h⟩ 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) rfl All goals completed! 🐙 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
right_inv := by n:ℕf:{ f // Function.Involutive f }⊢ Function.RightInverse
(fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
rintro (_ | ⟨i, h⟩) none n:ℕf:{ f // Function.Involutive f }⊢ (fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
((fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
none) =
nonesome n:ℕf:{ f // Function.Involutive f }i:Fin nh:↑f i = i⊢ (fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
((fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
(some ⟨i, h⟩)) =
some ⟨i, h⟩ 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) <;> none n:ℕf:{ f // Function.Involutive f }⊢ (fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
((fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
none) =
nonesome n:ℕf:{ f // Function.Involutive f }i:Fin nh:↑f i = i⊢ (fun i =>
match i with
| ⟨some i, h⟩ => some ⟨i, ⋯⟩
| ⟨none, h⟩ => none)
((fun i =>
match i with
| some ⟨i, h⟩ => ⟨some i, ⋯⟩
| none => ⟨none, ⋯⟩)
(some ⟨i, h⟩)) =
some ⟨i, h⟩ 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card) rfl All goals completed! 🐙 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f 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 := ⋯ }⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
let s : Finset (Fin n) := Finset.univ.filter fun i => f.1 i = i 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}⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
let e2' : { i : Fin n // f.1 i = i} ≃ {i // i ∈ s} := by 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}⊢ { i // ↑f i = i } ≃ ↥s 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 ⋯⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
apply Equiv.subtypeEquivProp 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}⊢ (fun i => ↑f i = i) = fun i => i ∈ s 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 ⋯⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
simp [s] 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 ⋯⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f 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 ⋯⊢ { i // ∀ (h : i.isSome = true), ↑f (i.get h) = i.get h } ≃ Option (Fin {i | ↑f i = i}.card)
let e2 : {i // i ∈ s} ≃ Fin (Finset.card s) := by 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 ⋯⊢ ↥s ≃ Fin s.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)
refine (Finset.orderIsoOfFin _ ?_).symm.toEquiv 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 ⋯⊢ s.card = s.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)
simp [s] 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) 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)
refine e1.trans (Equiv.optionCongr (e2'.trans (e2))) 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⟩ := by n:ℕ⊢ ∀ {f : { f // Function.Involutive f }},
(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none → ↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩
intro f h n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = none⊢ ↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩
by_contra hf0 n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonehf0:¬↑f ⟨0, ⋯⟩ = ⟨0, ⋯⟩⊢ False
simp only [Fin.zero_eta] at hf0 n:ℕf:{ f // Function.Involutive f }h:(involutionAddEquiv ((involutionCons n) f).fst) ((involutionCons n) f).snd = nonehf0:¬↑f 0 = 0⊢ False
simp only [succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv,
Option.isSome_some, Option.get_some, Option.isSome_none, dif_neg hf0] at h 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
exact absurd h (Option.some_ne_none _) All goals completed! 🐙
lemma involutionAddEquiv_cast {n : ℕ} {f1 f2 : {f : Fin n → Fin n // Function.Involutive f}}
(hf : f1 = f2) :
involutionAddEquiv f1 = (Equiv.subtypeEquivRight (by n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ ∀ (x : Option (Fin n)),
(∀ (h : x.isSome = true), ↑f1 (x.get h) = x.get h) ↔ ∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h rw [hf n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ ∀ (x : Option (Fin n)),
(∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h) ↔ ∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ ∀ (x : Option (Fin n)),
(∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h) ↔ ∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h] n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ ∀ (x : Option (Fin n)),
(∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h) ↔ ∀ (h : x.isSome = true), ↑f2 (x.get h) = x.get h; simp All goals completed! 🐙)).trans
((involutionAddEquiv f2).trans (Equiv.optionCongr (finCongr (by n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ {i | ↑f2 i = i}.card = {i | ↑f1 i = i}.card rw [hf n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ {i | ↑f2 i = i}.card = {i | ↑f2 i = i}.card All goals completed! 🐙] All goals completed! 🐙)))) := by n:ℕf1:{ f // Function.Involutive f }f2:{ f // Function.Involutive f }hf:f1 = f2⊢ involutionAddEquiv f1 = (Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f2).trans (finCongr ⋯).optionCongr)
subst hf n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 = (Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (finCongr ⋯).optionCongr)
rw [finCongr_refl, n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 =
(Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (Equiv.refl (Fin {i | ↑f1 i = i}.card)).optionCongr) n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 =
(Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (Equiv.refl (Option (Fin {i | ↑f1 i = i}.card)))) Equiv.optionCongr_refl n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 =
(Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (Equiv.refl (Option (Fin {i | ↑f1 i = i}.card)))) n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 =
(Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (Equiv.refl (Option (Fin {i | ↑f1 i = i}.card))))] n:ℕf1:{ f // Function.Involutive f }⊢ involutionAddEquiv f1 =
(Equiv.subtypeEquivRight ⋯).trans ((involutionAddEquiv f1).trans (Equiv.refl (Option (Fin {i | ↑f1 i = i}.card))))
rfl 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)) := by 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)
subst hf 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)
rfl 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 := by 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
simp only [succ_eq_add_one, involutionCons, Fin.cons_update, Equiv.coe_fn_mk, dite_eq_left_iff] 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
have hx : ¬ f.1 x.succ = ⟨0, Nat.zero_lt_succ n⟩:=
involutionAddEquiv_none_image_zero h ▸
fun hn => Fin.succ_ne_zero x (Function.Involutive.injective f.2 hn) 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 ↦ by 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 simp [h2] 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, by 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 simpa using f.2.2 All goals completed! 🐙⟩⟩
invFun f := ⟨f.2.1, ⟨f.2.2.1, f.2.2.2.1⟩⟩
left_inv f := rfl
right_inv f := by 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 ext a 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.fsta n:ℕ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✝) <;> a 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.fsta n:ℕ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 aesop 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.
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) ∧ f 0 = k.succ} ≃
{f : Fin n.succ → Fin n.succ // Function.Involutive (e.symm ∘ f ∘ e) ∧
(∀ i, (e.symm ∘ f ∘ e) i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} where
toFun f := ⟨e ∘ f.1 ∘ e.symm, by 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 }⊢ Function.Involutive (⇑e.symm ∘ (⇑e ∘ ↑f ∘ ⇑e.symm) ∘ ⇑e)
intro i 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) ((⇑e.symm ∘ (⇑e ∘ ↑f ∘ ⇑e.symm) ∘ ⇑e) i) = i
simp only [succ_eq_add_one, ne_eq, Function.comp_apply, Equiv.symm_apply_apply] 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⊢ ↑f (↑f i) = i
rw [f.2.1 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⊢ i = i All goals completed! 🐙] All goals completed! 🐙, by 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 simpa using f.2.2.1 All goals completed! 🐙, by 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 simpa using f.2.2.2 All goals completed! 🐙⟩
invFun f := ⟨e.symm ∘ f.1 ∘ e, by 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)
intro i 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
simpa using f.2.1 i All goals completed! 🐙, by 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 simpa using f.2.2.1 All goals completed! 🐙, by 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 simpa using f.2.2.2 All goals completed! 🐙⟩
left_inv f := by 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 ext i 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); simp All goals completed! 🐙
right_inv f := by 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 ext i 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); simp 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.
def involutionNoFixedZeroSetEquivSetEquiv {n : ℕ} (k : Fin n)
(e : Fin n.succ ≃ Fin n.succ) :
{f : Fin n.succ → Fin n.succ // Function.Involutive (e.symm ∘ f ∘ e) ∧
(∀ i, (e.symm ∘ f ∘ e) i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} ≃
{f : Fin n.succ → Fin n.succ // Function.Involutive f ∧
(∀ i, f i ≠ i) ∧ (e.symm ∘ f ∘ e) 0 = k.succ} := by n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succ⊢ { f //
Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧
(∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ } ≃
{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ }
refine Equiv.subtypeEquivRight fun f ↦ ?_ n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succ⊢ 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 f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ
have h1 : Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ↔ Function.Involutive f := by n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succ⊢ { f //
Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) ∧
(∀ (i : Fin n.succ), (⇑e.symm ∘ f ∘ ⇑e) i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ } ≃
{ f // 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 (⇑e.symm ∘ f ∘ ⇑e) ∧
(∀ (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
apply Iff.intro mp n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succ⊢ Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) → Function.Involutive fmpr n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succ⊢ Function.Involutive f → Function.Involutive (⇑e.symm ∘ f ∘ ⇑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 (⇑e.symm ∘ f ∘ ⇑e) ∧
(∀ (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 <;> mp n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succ⊢ Function.Involutive (⇑e.symm ∘ f ∘ ⇑e) → Function.Involutive fmpr n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succ⊢ Function.Involutive f → Function.Involutive (⇑e.symm ∘ f ∘ ⇑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 (⇑e.symm ∘ f ∘ ⇑e) ∧
(∀ (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 intro h i mpr n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh:Function.Involutive fi:Fin n.succ⊢ (⇑e.symm ∘ f ∘ ⇑e) ((⇑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 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 f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ
· mp n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh:Function.Involutive (⇑e.symm ∘ f ∘ ⇑e)i:Fin n.succ⊢ f (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 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 f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ simpa using h (e.symm 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 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 f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ
· mpr n:ℕk:Fin ne:Fin n.succ ≃ Fin n.succf:Fin n.succ → Fin n.succh:Function.Involutive fi:Fin n.succ⊢ (⇑e.symm ∘ f ∘ ⇑e) ((⇑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 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 f ∧ (∀ (i : Fin n.succ), f i ≠ i) ∧ (⇑e.symm ∘ f ∘ ⇑e) 0 = k.succ simp [h (e 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 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 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 (⇑e.symm ∘ f ∘ ⇑e) ∧
(∀ (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
rw [h1 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 ∧ (∀ (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 ∧ (∀ (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
simp only [succ_eq_add_one, Function.comp_apply, ne_eq, and_congr_right_iff, and_congr_left_iff] 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)
intro h1 h2 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
apply Iff.intro mp 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 = impr 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
· mp 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 intro h i mp 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
simpa using h (e.symm i) All goals completed! 🐙
· mpr 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 intro h i mpr 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
have hi := h (e i) mpr 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
by_contra hn mpr 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
nth_rewrite 2 [← hn] at hi mpr 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
simp at hi 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} := by 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 }
refine Equiv.subtypeEquivRight ?_ 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
simp only [succ_eq_add_one, ne_eq, Function.comp_apply, and_congr_right_iff] 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)
intro f hi h1 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
exact Equiv.symm_apply_eq e 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.
def involutionNoFixedZeroSetEquivSetOne {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.succ.succ → Fin n.succ.succ // Function.Involutive f ∧
(∀ i, f i ≠ i) ∧ f 0 = 1} := by n:ℕk:Fin n.succ⊢ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = k.succ } ≃
{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }
refine (involutionNoFixedZeroSetEquivEquiv k (Equiv.swap k.succ 1)).trans ?_ n:ℕk:Fin n.succ⊢ { f //
Function.Involutive (⇑(Equiv.symm (Equiv.swap k.succ 1)) ∘ f ∘ ⇑(Equiv.swap k.succ 1)) ∧
(∀ (i : Fin n.succ.succ), (⇑(Equiv.symm (Equiv.swap k.succ 1)) ∘ f ∘ ⇑(Equiv.swap k.succ 1)) i ≠ i) ∧
(⇑(Equiv.symm (Equiv.swap k.succ 1)) ∘ f ∘ ⇑(Equiv.swap k.succ 1)) 0 = k.succ } ≃
{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }
refine (involutionNoFixedZeroSetEquivSetEquiv k (Equiv.swap k.succ 1)).trans ?_ n:ℕk:Fin n.succ⊢ { f //
Function.Involutive f ∧
(∀ (i : Fin n.succ.succ), f i ≠ i) ∧
(⇑(Equiv.symm (Equiv.swap k.succ 1)) ∘ f ∘ ⇑(Equiv.swap k.succ 1)) 0 = k.succ } ≃
{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }
refine (involutionNoFixedZeroSetEquivEquiv' k (Equiv.swap k.succ 1)).trans ?_ n:ℕk:Fin n.succ⊢ { f //
Function.Involutive f ∧
(∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f ((Equiv.swap k.succ 1) 0) = (Equiv.swap k.succ 1) k.succ } ≃
{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }
refine Equiv.subtypeEquivRight ?_ n:ℕk:Fin n.succ⊢ ∀ (x : Fin n.succ.succ → Fin n.succ.succ),
Function.Involutive x ∧
(∀ (i : Fin n.succ.succ), x i ≠ i) ∧ x ((Equiv.swap k.succ 1) 0) = (Equiv.swap k.succ 1) k.succ ↔
Function.Involutive x ∧ (∀ (i : Fin n.succ.succ), x i ≠ i) ∧ x 0 = 1
simp only [succ_eq_add_one, ne_eq, Equiv.swap_apply_left, and_congr_right_iff] n:ℕk:Fin n.succ⊢ ∀ (x : Fin (n + 1 + 1) → Fin (n + 1 + 1)),
Function.Involutive x → (∀ (i : Fin (n + 1 + 1)), ¬x i = i) → (x ((Equiv.swap k.succ 1) 0) = 1 ↔ x 0 = 1)
intro f hi h1 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⊢ f ((Equiv.swap k.succ 1) 0) = 1 ↔ f 0 = 1
rw [Equiv.swap_apply_of_ne_of_ne 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⊢ f 0 = 1 ↔ f 0 = 1a 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.succa 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 a 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.succa 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] a 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.succa 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
· a 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 exact Ne.symm (Fin.succ_ne_zero k) All goals completed! 🐙
· a 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 exact Fin.zero_ne_one All goals completed! 🐙
Fixed point involutions of Fin n.succ.succ fixing f 0 = 1 are equivalent to
fixed point involutions of Fin n.
def involutionNoFixedSetOne {n : ℕ} :
{f : Fin n.succ.succ → Fin n.succ.succ // Function.Involutive f ∧
(∀ i, f i ≠ i) ∧ f 0 = 1} ≃ {f : Fin n → Fin n // Function.Involutive f ∧
(∀ i, f i ≠ i)} where
toFun f := by n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
have f_succ_succ_ne_zero_one (i : Fin n) : f.1 i.succ.succ ≠ 0 ∧ f.1 i.succ.succ ≠ 1 := by
have hf1 : f.1 1 = 0 := by n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0⊢ ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
simp only [← f.2.2.2] n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin n⊢ ↑f (↑f 0) = 0 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0⊢ ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
rw [f.2.1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin n⊢ 0 = 0 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0⊢ ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }] n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0⊢ ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0⊢ ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
refine ⟨fun hn => ?_, fun hn => ?_⟩ refine_1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0hn:↑f i.succ.succ = 0⊢ Falserefine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0hn:↑f i.succ.succ = 1⊢ False n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
· refine_1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0hn:↑f i.succ.succ = 0⊢ False n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } simpa [Fin.ext_iff] using f.2.1.injective (hn.trans hf1.symm) All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
· refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }i:Fin nhf1:↑f 1 = 0hn:↑f i.succ.succ = 1⊢ False n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } simpa [Fin.ext_iff] using f.2.1.injective (hn.trans f.2.2.2.symm) n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
let f' := f.1 ∘ Fin.succ ∘ Fin.succ n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succ⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
have hf' (i : Fin n) : f' i ≠ 0 := (f_succ_succ_ne_zero_one i).1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
let f'' := fun i => (f' i).pred (hf' i) n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
have hf'' (i : Fin n) : f'' i ≠ 0 := by
rw [ne_eq, n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f'' i = 0 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f' i = 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } Fin.pred_eq_iff_eq_succ, n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f' i = Fin.succ 0 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f' i = 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } Fin.succ_zero_eq_one n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f' i = 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f' i = 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }] n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯i:Fin n⊢ ¬f' i = 1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
exact (f_succ_succ_ne_zero_one i).2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
let f''' := fun i => (f'' i).pred (hf'' i) n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯⊢ { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
refine ⟨f''', ?_, ?_⟩ refine_1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯⊢ Function.Involutive f'''refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯⊢ ∀ (i : Fin n), f''' i ≠ i
· refine_1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯⊢ Function.Involutive f''' intro i refine_1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ f''' (f''' i) = i
simp only [succ_eq_add_one, ne_eq, Function.comp_apply, Fin.succ_pred, f''', f'', f'] refine_1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ((↑f (↑f i.succ.succ)).pred ⋯).pred ⋯ = i
simp [f.2.1 i.succ.succ] All goals completed! 🐙
· refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯⊢ ∀ (i : Fin n), f''' i ≠ i intro i refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ f''' i ≠ i
simp only [succ_eq_add_one, ne_eq, Function.comp_apply, f''', f'', f'] refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ¬((↑f i.succ.succ).pred ⋯).pred ⋯ = i
rw [Fin.pred_eq_iff_eq_succ, refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ¬(↑f i.succ.succ).pred ⋯ = i.succ refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ¬↑f i.succ.succ = i.succ.succ Fin.pred_eq_iff_eq_succ refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ¬↑f i.succ.succ = i.succ.succrefine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ¬↑f i.succ.succ = i.succ.succ]refine_2 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }f_succ_succ_ne_zero_one:∀ (i : Fin n), ↑f i.succ.succ ≠ 0 ∧ ↑f i.succ.succ ≠ 1f':Fin n → Fin n.succ.succ := ↑f ∘ Fin.succ ∘ Fin.succhf':∀ (i : Fin n), f' i ≠ 0f'':Fin n → Fin (n + 1) := fun i => (f' i).pred ⋯hf'':∀ (i : Fin n), f'' i ≠ 0f''':Fin n → Fin n := fun i => (f'' i).pred ⋯i:Fin n⊢ ¬↑f i.succ.succ = i.succ.succ
exact f.2.2.1 i.succ.succ All goals completed! 🐙
invFun f := by n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }
let f' := fun (i : Fin n.succ.succ)=>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨(Nat.succ (Nat.succ n)), h⟩ => (f.1 ⟨n, by n✝:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }i:Fin n✝.succ.succn:ℕh:n.succ.succ < n✝.succ.succ⊢ n < n✝ n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 } omega All goals completed! 🐙 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }⟩).succ.succ n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ { f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }
refine ⟨f', ?_, ?_, ?_⟩ refine_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ Function.Involutive f'refine_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ ∀ (i : Fin n.succ.succ), f' i ≠ irefine_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ f' 0 = 1
· refine_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ Function.Involutive f' intro i refine_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succ⊢ f' (f' i) = i
match i with
| ⟨0, h⟩ => n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succ⊢ f' (f' ⟨0, h⟩) = ⟨0, h⟩ rfl All goals completed! 🐙
| ⟨1, h⟩ => n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succ⊢ f' (f' ⟨1, h⟩) = ⟨1, h⟩ rfl All goals completed! 🐙
| ⟨(Nat.succ (Nat.succ m)), h⟩ => n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succ⊢ f' (f' ⟨m.succ.succ, h⟩) = ⟨m.succ.succ, h⟩
simp only [succ_eq_add_one, ne_eq, f'] n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succ⊢ (match (↑f ⟨m, ⋯⟩).succ.succ with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ) =
⟨m + 1 + 1, h⟩
split h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:(↑f ⟨m, ⋯⟩).succ.succ = ⟨0, h✝⟩⊢ 1 = ⟨m + 1 + 1, h⟩h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:(↑f ⟨m, ⋯⟩).succ.succ = ⟨1, h✝⟩⊢ 0 = ⟨m + 1 + 1, h⟩h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:(↑f ⟨m, ⋯⟩).succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ (↑f ⟨n✝, ⋯⟩).succ.succ = ⟨m + 1 + 1, h⟩
· h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:(↑f ⟨m, ⋯⟩).succ.succ = ⟨0, h✝⟩⊢ 1 = ⟨m + 1 + 1, h⟩ rename_i h h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝¹:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succh:(↑f ⟨m, ⋯⟩).succ.succ = ⟨0, h✝⟩⊢ 1 = ⟨m + 1 + 1, h⟩
simp [Fin.ext_iff] at h All goals completed! 🐙
· h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:(↑f ⟨m, ⋯⟩).succ.succ = ⟨1, h✝⟩⊢ 0 = ⟨m + 1 + 1, h⟩ rename_i h h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝¹:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succh:(↑f ⟨m, ⋯⟩).succ.succ = ⟨1, h✝⟩⊢ 0 = ⟨m + 1 + 1, h⟩
simp [Fin.ext_iff] at h All goals completed! 🐙
· h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:(↑f ⟨m, ⋯⟩).succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ (↑f ⟨n✝, ⋯⟩).succ.succ = ⟨m + 1 + 1, h⟩ rename_i h h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝¹:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succh:(↑f ⟨m, ⋯⟩).succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ (↑f ⟨n✝, ⋯⟩).succ.succ = ⟨m + 1 + 1, h⟩
rename_i x r h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:(↑f ⟨m, ⋯⟩).succ.succ = ⟨n✝.succ.succ, h✝⟩⊢ (↑f ⟨n✝, ⋯⟩).succ.succ = ⟨m + 1 + 1, h⟩
simp_all only [succ_eq_add_one, Fin.ext_iff, Fin.val_succ, add_left_inj] h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = x⊢ ↑(↑f ⟨x, ⋯⟩) = m
have ht : f.1 ⟨m, by n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = x⊢ m < n h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑(↑f ⟨x, ⋯⟩) = m omega All goals completed! 🐙h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑(↑f ⟨x, ⋯⟩) = m⟩ = ⟨x, by n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = x⊢ x < nh_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑(↑f ⟨x, ⋯⟩) = m omega All goals completed! 🐙h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑(↑f ⟨x, ⋯⟩) = m⟩ := Fin.ext hh_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑(↑f ⟨x, ⋯⟩) = m
rw [← ht, h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑(↑f (↑f ⟨m, ⋯⟩)) = m All goals completed! 🐙 f.2.1 h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh✝:m.succ.succ < n.succ.succi✝:Fin n✝.succ.succx:ℕr:n✝.succ.succ < n.succ.succh:↑(↑f ⟨m, ⋯⟩) = xht:↑f ⟨m, ⋯⟩ = ⟨x, ⋯⟩⊢ ↑⟨m, ⋯⟩ = m All goals completed! 🐙] All goals completed! 🐙
· refine_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ ∀ (i : Fin n.succ.succ), f' i ≠ i intro i refine_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succ⊢ f' i ≠ i
match i with
| ⟨0, h⟩ => n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succ⊢ f' ⟨0, h⟩ ≠ ⟨0, h⟩
simp only [succ_eq_add_one, ne_eq, Fin.zero_eta, f'] n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succ⊢ ¬(match 0 with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ) =
0
split h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:0 = ⟨0, h✝⟩⊢ ¬1 = 0h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:0 = ⟨1, h✝⟩⊢ ¬0 = 0h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:0 = ⟨n✝.succ.succ, h✝⟩⊢ ¬(↑f ⟨n✝, ⋯⟩).succ.succ = 0 <;> h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:0 = ⟨0, h✝⟩⊢ ¬1 = 0h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:0 = ⟨1, h✝⟩⊢ ¬0 = 0h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:0 < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:0 = ⟨n✝.succ.succ, h✝⟩⊢ ¬(↑f ⟨n✝, ⋯⟩).succ.succ = 0 try simp_all All goals completed! 🐙
| ⟨1, h⟩ => n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succ⊢ f' ⟨1, h⟩ ≠ ⟨1, h⟩
simp only [succ_eq_add_one, ne_eq, Fin.mk_one, f'] n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succ⊢ ¬(match 1 with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ) =
1
split h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:1 = ⟨0, h✝⟩⊢ ¬1 = 1h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:1 = ⟨1, h✝⟩⊢ ¬0 = 1h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:1 = ⟨n✝.succ.succ, h✝⟩⊢ ¬(↑f ⟨n✝, ⋯⟩).succ.succ = 1 <;> h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:1 = ⟨0, h✝⟩⊢ ¬1 = 1h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:1 = ⟨1, h✝⟩⊢ ¬0 = 1h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succh:1 < n.succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:1 = ⟨n✝.succ.succ, h✝⟩⊢ ¬(↑f ⟨n✝, ⋯⟩).succ.succ = 1 try simp_all All goals completed! 🐙
| ⟨(Nat.succ (Nat.succ m)), h⟩ => n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succ⊢ f' ⟨m.succ.succ, h⟩ ≠ ⟨m.succ.succ, h⟩
simp only [succ_eq_add_one, ne_eq, Fin.ext_iff, Fin.val_succ, add_left_inj, f'] n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succ⊢ ¬↑(↑f ⟨m, ⋯⟩) = m
have hf := f.2.2 ⟨m, Nat.add_lt_add_iff_right.mp h⟩ n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succhf:↑f ⟨m, ⋯⟩ ≠ ⟨m, ⋯⟩⊢ ¬↑(↑f ⟨m, ⋯⟩) = m
simp only [ne_eq, Fin.ext_iff] at hf n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi:Fin n✝.succ.succm:ℕh:m.succ.succ < n.succ.succhf:¬↑(↑f ⟨m, ⋯⟩) = m⊢ ¬↑(↑f ⟨m, ⋯⟩) = m
omega All goals completed! 🐙
· refine_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ f' 0 = 1 simp only [succ_eq_add_one, ne_eq, f'] refine_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ⊢ (match 0 with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succ) =
1
split h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:0 = ⟨0, h✝⟩⊢ 1 = 1h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:0 = ⟨1, h✝⟩⊢ 0 = 1h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:0 = ⟨n✝.succ.succ, h✝⟩⊢ (↑f ⟨n✝, ⋯⟩).succ.succ = 1 <;> h_1 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi✝:Fin n✝.succ.succh✝:0 < n.succ.succheq✝:0 = ⟨0, h✝⟩⊢ 1 = 1h_2 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi✝:Fin n✝.succ.succh✝:1 < n.succ.succheq✝:0 = ⟨1, h✝⟩⊢ 0 = 1h_3 n:ℕf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }f':Fin n.succ.succ → Fin (n + 1 + 1) :=
fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => (↑f ⟨n_1, ⋯⟩).succ.succi✝:Fin n✝.succ.succn✝:ℕh✝:n✝.succ.succ < n.succ.succheq✝:0 = ⟨n✝.succ.succ, h✝⟩⊢ (↑f ⟨n✝, ⋯⟩).succ.succ = 1 try simp_all All goals completed! 🐙
left_inv f := by n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }⊢ (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
have hf1 : f.1 1 = 0 := by
simp only [succ_eq_add_one, ne_eq, ← f.2.2.2] n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }⊢ ↑f (↑f 0) = 0 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
rw [f.2.1 n:ℕf:{ f // Function.Involutive f ∧ (∀ (i : Fin n.succ.succ), f i ≠ i) ∧ f 0 = 1 }⊢ 0 = 0 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 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 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
simp only [succ_eq_add_one, ne_eq, Function.comp_apply, Fin.succ_mk, Fin.succ_pred] 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
ext 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)⊢ ↑(↑⟨fun i =>
match i with
| ⟨0, h⟩ => 1
| ⟨1, h⟩ => 0
| ⟨n_1.succ.succ, h⟩ => ↑f ⟨n_1 + 1 + 1, ⋯⟩,
⋯⟩
i) =
↑(↑f i)
simp only 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)
split h_1 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✝⟩)h_2 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✝⟩)h_3 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✝⟩)
· h_1 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✝⟩) simp [succ_eq_add_one, Fin.zero_eta, f.2.2.2] All goals completed! 🐙
· h_2 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✝⟩) exact congrArg Fin.val hf1.symm All goals completed! 🐙
· h_3 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✝⟩) exact rfl All goals completed! 🐙
right_inv f := by 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
simp only [ne_eq, succ_eq_add_one, Function.comp_apply] 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
ext i 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)
simp only [Fin.val_pred] 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)
split h_1 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)h_2 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)h_3 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)
· h_1 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) rename_i h h_1 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)
simp [Fin.ext_iff] at h All goals completed! 🐙
· h_2 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) rename_i h h_2 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)
simp [Fin.ext_iff] at h All goals completed! 🐙
· h_3 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) simp only [Fin.val_succ, add_tsub_cancel_right] h_3 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)
congr h_3 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
apply congrArg h_3 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
simp_all [Fin.ext_iff] 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 } := by n:ℕ⊢ Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
have : DecidablePred fun x ↦ Function.Involutive x :=
fun f ↦ Fintype.decidableForallFintype (α := Fin n) n:ℕthis:DecidablePred fun x => Function.Involutive x⊢ Fintype { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }
exact Subtype.fintype .. 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)} := by 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 }
simp [Fintype.card_congr involutionNoFixedZeroEquivProd] 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
| Nat.succ n => n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ)), f i ≠ i } = (2 * n.succ - 1)‼ by n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ)), f i ≠ i } = (2 * n.succ - 1)‼
erw [involutionNoFixed_card_succ, 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)‼ involutionNoFixed_card_mul_two n 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)‼
exact (Nat.doubleFactorial_add_one (Nat.mul 2 n)).symm 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
| Nat.succ n => n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ + 1)), f i ≠ i } = 0 by n:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * n.succ + 1)), f i ≠ i } = 0
erw [involutionNoFixed_card_succ, n:ℕ⊢ (Nat.mul 2 n + 1).succ * Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (Nat.mul 2 n + 1)), f i ≠ i } = 0 involutionNoFixed_card_mul_two_plus_one n n:ℕ⊢ (Nat.mul 2 n + 1).succ * 0 = 0] n:ℕ⊢ (Nat.mul 2 n + 1).succ * 0 = 0
ring All goals completed! 🐙
lemma involutionNoFixed_card_even : (n : ℕ) → (he : Even n) →
Fintype.card {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} = (n - 1)‼ := by ⊢ ∀ (n : ℕ), Even n → Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼
intro n he n:ℕhe:Even n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼
obtain ⟨r, hr⟩ := he n:ℕr:ℕhr:n = r + r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼
have hr' : n = 2 * r := by ⊢ ∀ (n : ℕ), Even n → Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼ n:ℕr:ℕhr:n = r + rhr':n = 2 * r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼ omega n:ℕr:ℕhr:n = r + rhr':n = 2 * r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼ n:ℕr:ℕhr:n = r + rhr':n = 2 * r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼
subst hr' r:ℕhr:2 * r = r + r⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * r)), f i ≠ i } = (2 * r - 1)‼
exact involutionNoFixed_card_mul_two r 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 := by ⊢ ∀ (n : ℕ), Odd n → Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0
intro n ho n:ℕho:Odd n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0
obtain ⟨r, hr⟩ := ho n:ℕr:ℕhr:n = 2 * r + 1⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0
subst hr r:ℕ⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin (2 * r + 1)), f i ≠ i } = 0
exact involutionNoFixed_card_mul_two_plus_one r All goals completed! 🐙