`Compfiles/Usa2018P6.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

157 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2018, Problem 6

Let $a_n$ be the number of permutations $(x_1, x_2, \ldots, x_n)$ of the numbers $(1, 2, \ldots, n)$ such that the $n$ ratios $\frac{x_k}{k}$ for $1 \le k \le n$ are all distinct. Prove that $a_n$ is odd for all $n \ge 1$.

Imports (8)

Imported by 1 file

Compfiles.lean

def Usa2018P6.ratio The ratio x_k / k attached to position k of a permutation of {1, ..., n}, with positions and values encoded by Fin n via ·.val + 1 line 40 source
Source documentation
The ratio x_k / k attached to position k of a permutation of {1, ..., n}, with positions and values encoded by Fin n via ·.val + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Rat
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
```
def ratio {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : Fin n) : ℚ :=
…
```
def Usa2018P6.Valid A permutation is valid if all its ratios are distinct line 44 source
Source documentation
A permutation is valid if all its ratios are distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: Function.Injective, Rat, Usa2018P6.ratio

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Valid {n : ℕ} (σ : Equiv.Perm (Fin n)) : Prop :=
…
```
instance Usa2018P6.(instance at line 47) line 47 source
def Usa2018P6.nums The numerators of an involution: positions sent to a strictly larger value line 52 source
Source documentation
The numerators of an involution: positions sent to a strictly larger value.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Finset
Proof uses: Finset.filter, LT.lt, Finset.univ
7 instances, coercions and auxiliary constants left out.
```
def nums {n : ℕ} (σ : Equiv.Perm (Fin n)) : Finset (Fin n) :=
…
```
def Usa2018P6.label The label of the edge {k, σ k} as seen from its smaller endpoint k: the rational (k+1)/(σ k + 1) line 57 source
Source documentation
The label of the edge {k, σ k} as seen from its smaller endpoint k: the rational (k+1)/(σ k + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Rat
Proof uses: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
```
def label {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : Fin n) : ℚ :=
…
```
def Usa2018P6.Fantastic An involution is fantastic if its edges have pairwise distinct labels line 61 source
Source documentation
An involution is fantastic if its edges have pairwise distinct labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: Set.InjOn, Rat, Usa2018P6.label, Finset, Usa2018P6.nums
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def Fantastic {n : ℕ} (σ : Equiv.Perm (Fin n)) : Prop :=
…
```
instance Usa2018P6.(instance at line 64) line 64 source
def Usa2018P6.IsVertex A vertex is an involution with at most one fixed point (equivalently, a maximal matching of the complete graph) line 70 source
Source documentation
A vertex is an involution with at most one fixed point (equivalently, a maximal matching of the complete graph).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def IsVertex {n : ℕ} (σ : Equiv.Perm (Fin n)) : Prop :=
…
```
instance Usa2018P6.(instance at line 73) line 73 source
def Usa2018P6.IsSwitch A switching involution on a vertex σ: an involution φ supported on the numerators of σ which preserves labels line 79 source
Source documentation
A switching involution on a vertex σ: an involution φ supported on the numerators of σ which preserves labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: And, Function.Involutive, Not, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def IsSwitch {n : ℕ} (σ φ : Equiv.Perm (Fin n)) : Prop :=
…
```
instance Usa2018P6.(instance at line 83) line 83 source
def Usa2018P6.WPairs The type of pairs (σ, φ) with σ a vertex and φ a switching involution of σ line 88 source
Source documentation
The type of pairs (σ, φ) with σ a vertex and φ a switching involution of σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Prod, Equiv.Perm, Fin, And, Usa2018P6.IsVertex, Prod.fst, Usa2018P6.IsSwitch, Prod.snd

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def WPairs (n : ℕ) : Type :=
…
```
instance Usa2018P6.(instance at line 91) line 91 source
theorem Usa2018P6.even_card_of_involutive_ne A fixed-point-free involution on a fintype forces the cardinality to be even line 98 source
Source documentation
A fixed-point-free involution on a fintype forces the cardinality to be even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Function.Involutive, Ne, Even, Nat, Fintype.card
Proof uses: Equiv, Fin, Trunc.out, Fintype.truncEquivFin, Classical.propDecidable, Eq, Finset, Finset.filter, LT.lt, Finset.univ, rfl, Not, Finset.card, Finset.card_bij, Membership.mem, Eq.mpr, id, Eq.trans, And, congrFun' and 19 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
theorem even_card_of_involutive_ne {α : Type*} [Fintype α] {f : α → α}
    (hf : Function.Involutive f) (hfree : ∀ x, f x ≠ x) : Even (Fintype.card α) := by
…
```
Mentions: f
theorem Usa2018P6.card_modEq_of_involutive For an involution f on a fintype, the cardinality of the whole type is congruent modulo two to the cardinality of the fixed-point subtype line 130 source
Source documentation
For an involution f on a fintype, the cardinality of the whole type is congruent modulo two to the cardinality of the fixed-point subtype.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Function.Involutive, Nat.ModEq, OfNat.ofNat, Nat, Fintype.card, Subtype, Eq
Proof uses: HAdd.hAdd, Ne, Eq.mpr, HSub.hSub, id, congrArg, Not, Fintype.card_subtype_compl, Eq.symm, Nat.add_sub_of_le, Fintype.card_subtype_le, Even, Subtype.mk, Subtype.property, Eq.trans, Usa2018P6.even_card_of_involutive_ne, Subtype.ext, Iff.mp, Subtype.mk_eq_mk, HMod.hMod
14 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem card_modEq_of_involutive {α : Type*} [Fintype α] [DecidableEq α] (f : α → α)
    (hf : Function.Involutive f) :
    Fintype.card α ≡ Fintype.card {x // f x = x} [MOD 2] := by
…
```
Mentions: f
lemma Usa2018P6.val_add_one_pos line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LT.lt, Rat, OfNat.ofNat, HAdd.hAdd
Proof uses: Right.add_pos_of_nonneg_of_pos, Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.nat_mul_eq_of_label_eq Cross-multiplied form of an equality of labels line 158 source
Source documentation
Cross-multiplied form of an equality of labels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Eq, Rat, Usa2018P6.label, HMul.hMul, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mp, HDiv.hDiv, congrArg, propext, div_eq_div_iff, LT.lt.ne', Usa2018P6.val_add_one_pos, Usa2018P6.label.eq_1, cast, Eq.trans, congr, Eq.symm, Nat.cast_one
49 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma nat_mul_eq_of_label_eq {n : ℕ} {σ : Equiv.Perm (Fin n)} {x y : Fin n}
    (h : label σ x = label σ y) :
    (x.val + 1) * ((σ y).val + 1) = (y.val + 1) * ((σ x).val + 1) := by
…
```
Mentions: h, Usa2018P6.label
lemma Usa2018P6.lt_of_mul_eq_mul_lt If A * D = C * B with A < C then B < D (natural numbers) line 167 source
Source documentation
If A * D = C * B with A < C then B < D (natural numbers).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMul.hMul, LT.lt, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Nat.mul_comm, Eq.symm, Nat.mul_lt_mul_of_pos_right, Nat.lt_of_mul_lt_mul_right
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma lt_of_mul_eq_mul_lt {A B C D : ℕ} (h : A * D = C * B) (hAC : A < C) (hD : 0 < D) :
    B < D := by
…
```
Mentions: h
lemma Usa2018P6.eq_of_mul_eq_mul_eq If A * D = C * B with A = C and 0 < A then B = D line 175 source
Source documentation
If A * D = C * B with A = C and 0 < A then B = D.

standard axioms: propext what this means
Statement uses: Nat, Eq, HMul.hMul, LT.lt, OfNat.ofNat
Proof uses: Eq.symm, Nat.mul_left_cancel
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_mul_eq_mul_eq {A B C D : ℕ} (h : A * D = C * B) (hAC : A = C) (hA : 0 < A) :
    B = D := by
…
```
Mentions: h
lemma Usa2018P6.label_order_transfer Label equality transfers the order of numerators to the order of denominators line 181 source
Source documentation
Label equality transfers the order of numerators to the order of denominators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Eq, Rat, Usa2018P6.label, LT.lt
Proof uses: HMul.hMul, HAdd.hAdd, OfNat.ofNat, Usa2018P6.nat_mul_eq_of_label_eq, Usa2018P6.lt_of_mul_eq_mul_lt
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma label_order_transfer {n : ℕ} {σ : Equiv.Perm (Fin n)} {x y : Fin n}
    (h : label σ x = label σ y) :
    x.val < y.val → (σ x).val < (σ y).val := by
…
```
Mentions: h, Usa2018P6.label
lemma Usa2018P6.ratio_pos line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, LT.lt, Rat, OfNat.ofNat, Usa2018P6.ratio
Proof uses: id, div_pos, HAdd.hAdd, Right.add_pos_of_nonneg_of_pos, Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.valid_inv A permutation is valid iff its inverse is (one direction) line 196 source
Source documentation
A permutation is valid iff its inverse is (one direction).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.Valid, Inv.inv
Proof uses: Eq, Rat, Usa2018P6.ratio, of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.apply_symm_apply, eq_self, id, Eq.mpr, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, inv_div, Eq.refl, inv_injective, Eq.mp, Equiv.injective
21 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem valid_inv {n : ℕ} {σ : Equiv.Perm (Fin n)} (h : Valid σ) : Valid σ⁻¹ := by
…
```
Mentions: h, Usa2018P6.Valid
lemma Usa2018P6.ratio_eq_one_iff line 210 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Iff, Eq, Rat, Usa2018P6.ratio, OfNat.ofNat
Proof uses: id, Eq.mpr, HDiv.hDiv, HAdd.hAdd, congrArg, propext, div_eq_one_iff_eq, LT.lt.ne', Usa2018P6.val_add_one_pos, Iff.intro, cast, Eq.trans, congr, Eq.symm, Nat.cast_one, Fin.ext, Nat.succ.inj, Eq.refl
38 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.one_lt_ratio_iff line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Iff, LT.lt, Rat, OfNat.ofNat, Usa2018P6.ratio
Proof uses: id, Eq.mpr, HDiv.hDiv, HAdd.hAdd, Eq, congrArg, propext, one_lt_div, Usa2018P6.val_add_one_pos, Iff.intro, cast, Eq.trans, congr, Eq.symm, Nat.cast_one
59 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.ratio_lt_one_iff line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Iff, LT.lt, Rat, Usa2018P6.ratio, OfNat.ofNat
Proof uses: id, Eq.mpr, HDiv.hDiv, HAdd.hAdd, Eq, congrArg, propext, div_lt_one, Usa2018P6.val_add_one_pos, Iff.intro, cast, Eq.trans, congr, Eq.symm, Nat.cast_one
59 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.label_eq_ratio line 245 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Eq, Rat, Usa2018P6.label, Usa2018P6.ratio
Proof uses: id, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Eq.mpr, congrArg, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.mem_nums_iff line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Iff, Membership.mem, Finset, Usa2018P6.nums, LT.lt
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, And, Finset.univ, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, true_and, iff_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.fixed_or_num_or_denom For an involution, every element is fixed, a numerator, or a denominator line 255 source
Source documentation
For an involution, every element is fixed, a numerator, or a denominator.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Or, Eq, Membership.mem, Finset, Usa2018P6.nums
Proof uses: LT.lt, lt_trichotomy, Or.inr, Or.inl, Iff.mpr, Usa2018P6.mem_nums_iff, Fin.ext, Eq.symm, Eq.mpr, id, congrArg
17 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma fixed_or_num_or_denom {n : ℕ} {σ : Equiv.Perm (Fin n)}
    (hinv : Function.Involutive σ) (k : Fin n) :
    σ k = k ∨ k ∈ nums σ ∨ σ k ∈ nums σ := by
…
```
Mentions: Usa2018P6.nums
theorem Usa2018P6.valid_iff_of_involutive A valid involution has at most one fixed point and distinct edge labels; the converse also holds line 265 source
Source documentation
A valid involution has at most one fixed point and distinct edge labels; the converse also holds.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Iff, Usa2018P6.Valid, And, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, OfNat.ofNat, Usa2018P6.Fantastic
Proof uses: Iff.intro, And.intro, Eq.mpr, Membership.mem, Finset, id, congrArg, propext, Finset.card_le_one, Rat, Usa2018P6.ratio, Iff.mpr, Usa2018P6.ratio_eq_one_iff, Eq.mp, Eq.trans, True, congrFun', true_and, Eq.refl, Set and 69 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 78 steps
Open to load the checked before-and-after goal states.
```
theorem valid_iff_of_involutive {n : ℕ} {σ : Equiv.Perm (Fin n)}
    (hinv : Function.Involutive σ) :
    Valid σ ↔ (Finset.univ.filter fun x => σ x = x).card ≤ 1 ∧ Fantastic σ := by
…
```
Mentions: Usa2018P6.Valid, Usa2018P6.Fantastic
lemma Usa2018P6.list_prod_perms_apply_of_forall_fix line 347 source
standard axioms: Quot.sound, propext what this means
Statement uses: DecidableEq, List, Equiv.Perm, Membership.mem, Eq, List.prod, List.map
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, True, congrFun', congrArg, OfNat.ofNat, List.map_nil, eq_self, List.cons, Eq.mpr, id, List.map_cons, HMul.hMul, List.prod_cons, Equiv.Perm.mul_apply, List.mem_cons_of_mem, List.mem_cons_self, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.list_prod_swap_apply_left A product of swaps of pairwise disjoint pairs sends u i to v i line 357 source
Source documentation
A product of swaps of pairwise disjoint pairs sends u i to v i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, List.Nodup, Membership.mem, Ne, And, Eq, Equiv.Perm, List.prod, List.map, Equiv.swap
Proof uses: List.rec, List.nil, False.elim, Eq.mp, False, List.cons, Eq.mpr, id, congrArg, List.map_cons, HMul.hMul, List.prod_cons, Equiv.Perm.mul_apply, dite, Not, Eq.symm, And.left, Iff.mp, List.nodup_cons, Eq.rec and 10 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma list_prod_swap_apply_left [DecidableEq ι] (l : List ι) (u v : ι → α) (hnd : l.Nodup)
    (hd : ∀ i ∈ l, ∀ j ∈ l, i ≠ j → u i ≠ u j ∧ u i ≠ v j ∧ v i ≠ u j ∧ v i ≠ v j)
    (i : ι) (hi : i ∈ l) :
    ((l.map fun j => Equiv.swap (u j) (v j)).prod) (u i) = v i := by
…
```
lemma Usa2018P6.list_prod_swap_apply_right A product of swaps of pairwise disjoint pairs sends v i to u i line 388 source
Source documentation
A product of swaps of pairwise disjoint pairs sends v i to u i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, List.Nodup, Membership.mem, Ne, And, Eq, Equiv.Perm, List.prod, List.map, Equiv.swap
Proof uses: List.rec, List.nil, False.elim, Eq.mp, False, List.cons, Eq.mpr, id, congrArg, List.map_cons, HMul.hMul, List.prod_cons, Equiv.Perm.mul_apply, dite, Not, Eq.symm, And.left, Iff.mp, List.nodup_cons, Eq.rec and 10 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma list_prod_swap_apply_right [DecidableEq ι] (l : List ι) (u v : ι → α) (hnd : l.Nodup)
    (hd : ∀ i ∈ l, ∀ j ∈ l, i ≠ j → u i ≠ u j ∧ u i ≠ v j ∧ v i ≠ u j ∧ v i ≠ v j)
    (i : ι) (hi : i ∈ l) :
    ((l.map fun j => Equiv.swap (u j) (v j)).prod) (v i) = u i := by
…
```
lemma Usa2018P6.list_prod_swap_apply_of_not_mem A product of swaps fixes any point avoided by all the swaps line 419 source
Source documentation
A product of swaps fixes any point avoided by all the swaps.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, List, Membership.mem, And, Ne, Eq, Equiv.Perm, List.prod, List.map, Equiv.swap
Proof uses: Usa2018P6.list_prod_perms_apply_of_forall_fix, Equiv.swap_apply_of_ne_of_ne, And.left, And.right
7 instances, coercions and auxiliary constants left out.
```
lemma list_prod_swap_apply_of_not_mem [DecidableEq ι] (l : List ι) (u v : ι → α) (z : α)
    (hz : ∀ i ∈ l, z ≠ u i ∧ z ≠ v i) :
    ((l.map fun j => Equiv.swap (u j) (v j)).prod) z = z :=
…
```
def Usa2018P6.reps The representatives of the pairs switched by φ: the smaller element of each transposed pair of numerators line 431 source
Source documentation
The representatives of the pairs switched by φ: the smaller element of each transposed pair of numerators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Finset
Proof uses: Finset.filter, And, Ne, LT.lt, Eq, Usa2018P6.nums
9 instances, coercions and auxiliary constants left out.
```
def reps {n : ℕ} (σ φ : Equiv.Perm (Fin n)) : Finset (Fin n) :=
…
```
def Usa2018P6.conjPerm The conjugating permutation: the product of the swaps (σ x, φ x) over the representatives line 436 source
Source documentation
The conjugating permutation: the product of the swaps (σ x, φ x) over the representatives.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: List.prod, List.map, Equiv.swap, Finset.sort, Usa2018P6.reps, LE.le
11 instances, coercions and auxiliary constants left out.
```
def conjPerm {n : ℕ} (σ φ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin n) :=
…
```
def Usa2018P6.newSwitch The new switching involution: the product of the swaps (x, σ x) over the representatives line 441 source
Source documentation
The new switching involution: the product of the swaps (x, σ x) over the representatives.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: List.prod, List.map, Equiv.swap, Finset.sort, Usa2018P6.reps, LE.le
11 instances, coercions and auxiliary constants left out.
```
def newSwitch {n : ℕ} (σ φ : Equiv.Perm (Fin n)) : Equiv.Perm (Fin n) :=
…
```
lemma Usa2018P6.mem_reps line 444 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Iff, Membership.mem, Finset, Usa2018P6.reps, And, Usa2018P6.nums, Ne, LT.lt
Proof uses: of_eq_true, Eq.trans, Not, Eq, True, congr, congrArg, Finset.filter, congrFun', Finset.filter_congr, Iff.of_eq, iff_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.switch_mapsTo_nums A switching involution maps numerators to numerators line 449 source
Source documentation
A switching involution maps numerators to numerators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.nums
Proof uses: Decidable.byContradiction, Not, Eq, And.left, Rat, Usa2018P6.label, And.right, Function.Involutive, And, Eq.mp, congrArg, Eq.mpr, id
12 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma switch_mapsTo_nums {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hφ : IsSwitch σ φ) {x : Fin n} (hx : x ∈ nums σ) : φ x ∈ nums σ := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.nums
lemma Usa2018P6.denom_not_mem_nums The image of a numerator is not a numerator line 463 source
Source documentation
The image of a numerator is not a numerator.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Not
Proof uses: Eq.mpr, LE.le, id, Eq, Eq.trans, LT.lt, congrArg, Finset.filter, Finset.univ, And, True, congrFun', true_and, le_of_lt, Iff.mp, Usa2018P6.mem_nums_iff
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma denom_not_mem_nums {n : ℕ} {σ : Equiv.Perm (Fin n)} (hσ : Function.Involutive σ)
    {x : Fin n} (hx : x ∈ nums σ) : σ x ∉ nums σ := by
…
```
Mentions: Usa2018P6.nums
lemma Usa2018P6.reps_four_distinct The pairs (σ x, φ x) for distinct representatives are pairwise disjoint line 470 source
Source documentation
The pairs (σ x, φ x) for distinct representatives are pairwise disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Ne, And
Proof uses: Usa2018P6.nums, And.left, LT.lt, Iff.mp, Usa2018P6.mem_reps, And.intro, Eq, Equiv.injective, Usa2018P6.denom_not_mem_nums, Eq.rec, Usa2018P6.switch_mapsTo_nums, Eq.symm, Function.Involutive.injective, Not, Rat, Usa2018P6.label
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma reps_four_distinct {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ)
    {x y : Fin n} (hx : x ∈ reps σ φ) (hy : y ∈ reps σ φ) (hxy : x ≠ y) :
    σ x ≠ σ y ∧ σ x ≠ φ y ∧ φ x ≠ σ y ∧ φ x ≠ φ y := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps
lemma Usa2018P6.reps_four_distinct' The pairs (x, σ x) for distinct representatives are pairwise disjoint line 483 source
Source documentation
The pairs (x, σ x) for distinct representatives are pairwise disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Ne, And
Proof uses: Usa2018P6.nums, And.left, LT.lt, Iff.mp, Usa2018P6.mem_reps, And.intro, Eq, Usa2018P6.denom_not_mem_nums, Eq.rec, Eq.symm, Equiv.injective
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma reps_four_distinct' {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (_hφ : IsSwitch σ φ)
    {x y : Fin n} (hx : x ∈ reps σ φ) (hy : y ∈ reps σ φ) (hxy : x ≠ y) :
    x ≠ y ∧ x ≠ σ y ∧ σ x ≠ y ∧ σ x ≠ σ y := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps
lemma Usa2018P6.reps_four_distinct'' The pairs (x, φ x) for distinct representatives are pairwise disjoint line 496 source
Source documentation
The pairs (x, φ x) for distinct representatives are pairwise disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Ne, And
Proof uses: LT.lt, And.right, Usa2018P6.nums, Iff.mp, Usa2018P6.mem_reps, And.intro, Eq, Eq.trans, congrArg, And.left, Function.Involutive, Not, Rat, Usa2018P6.label, absurd, False, Eq.mp, not_lt_of_gt, Eq.symm, Function.Involutive.injective
13 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma reps_four_distinct'' {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hφ : IsSwitch σ φ)
    {x y : Fin n} (hx : x ∈ reps σ φ) (hy : y ∈ reps σ φ) (hxy : x ≠ y) :
    x ≠ y ∧ x ≠ φ y ∧ φ x ≠ y ∧ φ x ≠ φ y := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps
lemma Usa2018P6.conjPerm_apply_left line 514 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Eq, Usa2018P6.conjPerm
Proof uses: id, Usa2018P6.list_prod_swap_apply_left, Finset.sort, LE.le, Finset.sort_nodup, List, Ne, Usa2018P6.reps_four_distinct, Iff.mp, Finset.mem_sort, Iff.mpr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.conjPerm_apply_right line 524 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Eq, Usa2018P6.conjPerm
Proof uses: id, Usa2018P6.list_prod_swap_apply_right, Finset.sort, LE.le, Finset.sort_nodup, List, Ne, Usa2018P6.reps_four_distinct, Iff.mp, Finset.mem_sort, Iff.mpr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.conjPerm_apply_of_not_mem line 534 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Membership.mem, Finset, Usa2018P6.reps, And, Ne, Eq, Usa2018P6.conjPerm
Proof uses: id, Usa2018P6.list_prod_swap_apply_of_not_mem, Finset.sort, LE.le, List, Iff.mp, Finset.mem_sort
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.newSwitch_apply_left line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Eq, Usa2018P6.newSwitch
Proof uses: id, Usa2018P6.list_prod_swap_apply_left, Finset.sort, LE.le, Finset.sort_nodup, List, Ne, Usa2018P6.reps_four_distinct', Iff.mp, Finset.mem_sort, Iff.mpr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.newSwitch_apply_right line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Eq, Usa2018P6.newSwitch
Proof uses: id, Usa2018P6.list_prod_swap_apply_right, Finset.sort, LE.le, Finset.sort_nodup, List, Ne, Usa2018P6.reps_four_distinct', Iff.mp, Finset.mem_sort, Iff.mpr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.newSwitch_apply_of_not_mem line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Membership.mem, Finset, Usa2018P6.reps, And, Ne, Eq, Usa2018P6.newSwitch
Proof uses: id, Usa2018P6.list_prod_swap_apply_of_not_mem, Finset.sort, LE.le, List, Iff.mp, Finset.mem_sort
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.conjPerm_involutive line 568 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Usa2018P6.conjPerm
Proof uses: dite, Eq, Exists, And, Membership.mem, Finset, Usa2018P6.reps, Or, Or.inl, Eq.mpr, id, congrArg, Eq.symm, Usa2018P6.conjPerm_apply_left, Usa2018P6.conjPerm_apply_right, Eq.refl, Or.inr, Not, Usa2018P6.conjPerm_apply_of_not_mem, Ne and 8 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.newSwitch_involutive line 586 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Usa2018P6.newSwitch
Proof uses: dite, Eq, Exists, And, Membership.mem, Finset, Usa2018P6.reps, Or, Or.inl, Eq.mpr, id, congrArg, Eq.symm, Usa2018P6.newSwitch_apply_left, Usa2018P6.newSwitch_apply_right, Eq.refl, Or.inr, Not, Usa2018P6.newSwitch_apply_of_not_mem, Ne and 8 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.flip1_involutive The flipped involution π σ π is involutive line 605 source
Source documentation
The flipped involution π σ π is involutive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, HMul.hMul, Usa2018P6.conjPerm
Proof uses: Usa2018P6.conjPerm_involutive, id, Eq, Eq.mpr, congrArg, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma flip1_involutive {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) :
    Function.Involutive (conjPerm σ φ * σ * conjPerm σ φ) := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.conjPerm
lemma Usa2018P6.flip1_fixed_iff Fixed points of the flipped involution are the π-images of fixed points of σ line 614 source
Source documentation
Fixed points of the flipped involution are the π-images of fixed points of σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Iff, Eq, HMul.hMul, Usa2018P6.conjPerm
Proof uses: id, Function.Involutive.eq_iff, Usa2018P6.conjPerm_involutive
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma flip1_fixed_iff {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) (z : Fin n) :
    (conjPerm σ φ * σ * conjPerm σ φ) z = z ↔ σ (conjPerm σ φ z) = conjPerm σ φ z := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.conjPerm
lemma Usa2018P6.flip1_fixed_card The flipped involution has the same number of fixed points as σ line 621 source
Source documentation
The flipped involution has the same number of fixed points as σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Eq, Finset.card, Finset.filter, HMul.hMul, Usa2018P6.conjPerm, Finset.univ
Proof uses: Usa2018P6.conjPerm_involutive, Finset.card_bij, Membership.mem, Finset, Eq.mpr, id, Eq.trans, And, True, congrFun', congrArg, true_and, Iff.mp, Usa2018P6.flip1_fixed_iff, Eq.mp, Function.Involutive.injective, Exists.intro, Exists, propext
18 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma flip1_fixed_card {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) :
    (Finset.univ.filter fun x => (conjPerm σ φ * σ * conjPerm σ φ) x = x).card =
    (Finset.univ.filter fun x => σ x = x).card := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.conjPerm
lemma Usa2018P6.flip1_apply_of_mem_reps On a representative x, the flipped involution acts as φ line 640 source
Source documentation
On a representative x, the flipped involution acts as φ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Eq, HMul.hMul, Usa2018P6.conjPerm
Proof uses: Usa2018P6.conjPerm_apply_of_not_mem, Usa2018P6.nums, And.left, And, Ne, LT.lt, Iff.mp, Usa2018P6.mem_reps, And.intro, Usa2018P6.denom_not_mem_nums, Eq.rec, Eq.trans, congrArg, Not, Rat, Usa2018P6.label, And.right, absurd, False, Eq.mp and 6 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma flip1_apply_of_mem_reps {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ)
    {x : Fin n} (hx : x ∈ reps σ φ) :
    (conjPerm σ φ * σ * conjPerm σ φ) x = φ x := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps, Usa2018P6.conjPerm
lemma Usa2018P6.flip1_apply_denom_of_mem_reps On the denominator σ x of a representative, the flipped involution acts as σ ∘ φ line 664 source
Source documentation
On the denominator σ x of a representative, the flipped involution acts as σ ∘ φ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.reps, Eq, HMul.hMul, Usa2018P6.conjPerm
Proof uses: Usa2018P6.conjPerm_apply_of_not_mem, And.intro, Ne, Equiv.injective, Usa2018P6.nums, And, LT.lt, False, Iff.mp, Usa2018P6.mem_reps, Eq.mp, congrArg, Eq.symm, And.right, absurd, And.left, Not, Rat, Usa2018P6.label, not_lt_of_gt and 6 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma flip1_apply_denom_of_mem_reps {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ)
    {x : Fin n} (hx : x ∈ reps σ φ) :
    (conjPerm σ φ * σ * conjPerm σ φ) (σ x) = σ (φ x) := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps, Usa2018P6.conjPerm
lemma Usa2018P6.newSwitch_mem_nums_flip Points moved by the new switching involution are numerators of the flipped involution line 689 source
Source documentation
Points moved by the new switching involution are numerators of the flipped involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Ne, Usa2018P6.newSwitch, Membership.mem, Finset, Usa2018P6.nums, HMul.hMul, Usa2018P6.conjPerm
Proof uses: Exists, And, Usa2018P6.reps, Or, Eq, Decidable.byContradiction, Not, Usa2018P6.newSwitch_apply_of_not_mem, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, Eq.mpr, id, congrArg, LT.lt, propext and 11 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma newSwitch_mem_nums_flip {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) {z : Fin n}
    (hz : newSwitch σ φ z ≠ z) :
    z ∈ nums (conjPerm σ φ * σ * conjPerm σ φ) := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.newSwitch, Usa2018P6.nums, Usa2018P6.conjPerm
lemma Usa2018P6.flip2_label The new switching involution preserves labels of the flipped involution line 706 source
Source documentation
The new switching involution preserves labels of the flipped involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Membership.mem, Finset, Usa2018P6.nums, HMul.hMul, Usa2018P6.conjPerm, Eq, Rat, Usa2018P6.label, Usa2018P6.newSwitch
Proof uses: dite, Exists, And, Usa2018P6.reps, Or, Eq.mpr, id, congrArg, Usa2018P6.newSwitch_apply_left, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Usa2018P6.flip1_apply_denom_of_mem_reps, Usa2018P6.flip1_apply_of_mem_reps, And.right, Not, And.left, Ne, LT.lt, Iff.mp and 16 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma flip2_label {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) {z : Fin n}
    (_hz : z ∈ nums (conjPerm σ φ * σ * conjPerm σ φ)) :
    label (conjPerm σ φ * σ * conjPerm σ φ) (newSwitch σ φ z) =
    label (conjPerm σ φ * σ * conjPerm σ φ) z := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.nums, Usa2018P6.conjPerm, Usa2018P6.label, Usa2018P6.newSwitch
lemma Usa2018P6.reps_flip The representatives of the flipped pair are the original representatives line 734 source
Source documentation
The representatives of the flipped pair are the original representatives.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Eq, Finset, Usa2018P6.reps, HMul.hMul, Usa2018P6.conjPerm, Usa2018P6.newSwitch
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, Usa2018P6.nums, Ne, LT.lt, id, congr, congrArg, Iff.intro, Exists, Or, Decidable.byContradiction, Not, Usa2018P6.newSwitch_apply_of_not_mem, Eq.mp, Eq.trans, binderNameHint and 19 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma reps_flip {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) :
    reps (conjPerm σ φ * σ * conjPerm σ φ) (newSwitch σ φ) = reps σ φ := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps, Usa2018P6.conjPerm, Usa2018P6.newSwitch
lemma Usa2018P6.conjPerm_flip The conjugating permutation of the flipped pair is the original one line 765 source
Source documentation
The conjugating permutation of the flipped pair is the original one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Eq, Usa2018P6.conjPerm, HMul.hMul, Usa2018P6.newSwitch
Proof uses: id, Eq.mpr, List.prod, List.map, Equiv.swap, Finset.sort, Usa2018P6.reps, LE.le, congrArg, Finset, Usa2018P6.reps_flip, Mul, One, List, Eq.rec, Eq.refl, List.map_congr_left, Membership.mem, Usa2018P6.flip1_apply_of_mem_reps, Iff.mp and 3 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma conjPerm_flip {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) :
    conjPerm (conjPerm σ φ * σ * conjPerm σ φ) (newSwitch σ φ) = conjPerm σ φ := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.conjPerm, Usa2018P6.newSwitch
lemma Usa2018P6.eq_prod_swap_self A switching involution is the product of its own transpositions line 779 source
Source documentation
A switching involution is the product of its own transpositions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.IsSwitch, Eq, List.prod, List.map, Equiv.swap, Finset.sort, Usa2018P6.reps, LE.le
Proof uses: Equiv.Perm.ext, Fin.ext, dite, Exists, And, Membership.mem, Finset, Or, Eq.mpr, id, congrArg, Eq.symm, Usa2018P6.list_prod_swap_apply_left, Finset.sort_nodup, List, Ne, Usa2018P6.reps_four_distinct'', Iff.mp, Finset.mem_sort, Iff.mpr and 25 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma eq_prod_swap_self {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hφ : IsSwitch σ φ) :
    φ = (((reps σ φ).sort (· ≤ ·)).map fun x => Equiv.swap x (φ x)).prod := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.reps
lemma Usa2018P6.newSwitch_flip The new switching involution of the flipped pair is the original switching involution line 820 source
Source documentation
The new switching involution of the flipped pair is the original switching involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Eq, Usa2018P6.newSwitch, HMul.hMul, Usa2018P6.conjPerm
Proof uses: id, Eq.mpr, List.prod, List.map, Equiv.swap, Finset.sort, Usa2018P6.reps, LE.le, congrArg, Finset, Usa2018P6.reps_flip, Eq.rec, Eq.refl, Eq.trans, Usa2018P6.eq_prod_swap_self, Mul, One, List, List.map_congr_left, Membership.mem and 3 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma newSwitch_flip {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) :
    newSwitch (conjPerm σ φ * σ * conjPerm σ φ) (newSwitch σ φ) = φ := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.newSwitch, Usa2018P6.conjPerm
def Usa2018P6.flipPair The flip on pairs (σ, φ) line 833 source
Source documentation
The flip on pairs (σ, φ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Equiv.Perm, Fin
Proof uses: Prod.mk, HMul.hMul, Usa2018P6.conjPerm, Prod.fst, Prod.snd, Usa2018P6.newSwitch
2 instances, coercions and auxiliary constants left out.
```
def flipPair {n : ℕ} (p : Equiv.Perm (Fin n) × Equiv.Perm (Fin n)) :
    Equiv.Perm (Fin n) × Equiv.Perm (Fin n) :=
…
```
lemma Usa2018P6.flipPair_involutive_on The flip is an involution on valid pairs line 838 source
Source documentation
The flip is an involution on valid pairs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Eq, Prod, Usa2018P6.flipPair, Prod.mk
Proof uses: Usa2018P6.conjPerm, Usa2018P6.conjPerm_involutive, HMul.hMul, Usa2018P6.newSwitch, Usa2018P6.conjPerm_flip, Usa2018P6.newSwitch_flip, OfNat.ofNat, Equiv.Perm.ext, Fin.ext, id, congrArg, Prod.fst, Prod.snd, Eq.mpr, Eq.rec, Eq.refl, Trans.trans, of_eq_true, Eq.trans, True and 5 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma flipPair_involutive_on {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ) :
    flipPair (flipPair (σ, φ)) = (σ, φ) := by
…
```
Mentions: Usa2018P6.IsSwitch, Usa2018P6.flipPair
lemma Usa2018P6.flipPair_mem The flip preserves membership in the vertex-switching set line 859 source
Source documentation
The flip preserves membership in the vertex-switching set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.IsVertex, Usa2018P6.IsSwitch, And, HMul.hMul, Usa2018P6.conjPerm, Usa2018P6.newSwitch
Proof uses: Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, OfNat.ofNat, And.intro, Usa2018P6.flip1_involutive, Eq.mpr, id, congrArg, Usa2018P6.flip1_fixed_card, Not, Membership.mem, Finset, Usa2018P6.nums, Rat, Usa2018P6.label, Usa2018P6.newSwitch_involutive and 3 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma flipPair_mem {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : IsVertex σ) (hφ : IsSwitch σ φ) :
    IsVertex (conjPerm σ φ * σ * conjPerm σ φ) ∧
    IsSwitch (conjPerm σ φ * σ * conjPerm σ φ) (newSwitch σ φ) := by
…
```
Mentions: Usa2018P6.IsVertex, Usa2018P6.IsSwitch, Usa2018P6.conjPerm, Usa2018P6.newSwitch
lemma Usa2018P6.flipPair_eq_self_iff A fixed point of the flip has trivial switching involution line 872 source
Source documentation
A fixed point of the flip has trivial switching involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Usa2018P6.IsSwitch, Eq, Prod, Usa2018P6.flipPair, Prod.mk, OfNat.ofNat
Proof uses: Usa2018P6.newSwitch, congrArg, Prod.snd, Finset, Usa2018P6.reps, EmptyCollection.emptyCollection, Decidable.byContradiction, Not, Membership.mem, Finset.Nonempty, False, Iff.mpr, Ne, Finset.nonempty_iff_ne_empty, Eq.mpr, id, Eq.symm, Usa2018P6.newSwitch_apply_left, Usa2018P6.nums, Usa2018P6.switch_mapsTo_nums and 27 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma flipPair_eq_self_iff {n : ℕ} {σ φ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hφ : IsSwitch σ φ)
    (h : flipPair (σ, φ) = (σ, φ)) : φ = 1 := by
…
```
Mentions: Usa2018P6.IsSwitch, h, Usa2018P6.flipPair
lemma Usa2018P6.flipPair_eq_self_of_eq_one Any pair with trivial switching involution is a fixed point of the flip line 890 source
Source documentation
Any pair with trivial switching involution is a fixed point of the flip.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Eq, OfNat.ofNat, Prod, Usa2018P6.flipPair, Prod.mk
Proof uses: Finset, Usa2018P6.reps, EmptyCollection.emptyCollection, Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, False, True, congr, congrArg, congrFun', Finset.filter, And, Ne, LT.lt, Usa2018P6.nums, Finset.filter_congr, Iff.of_eq and 29 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma flipPair_eq_self_of_eq_one {n : ℕ} {σ φ : Equiv.Perm (Fin n)} (h : φ = 1) :
    flipPair (σ, φ) = (σ, φ) := by
…
```
Mentions: h, Usa2018P6.flipPair
lemma Usa2018P6.isSwitch_id The identity is a switching involution line 908 source
Source documentation
The identity is a switching involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.IsSwitch, OfNat.ofNat
Proof uses: And.intro, Function.Involutive, And, Not, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, of_eq_true, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma isSwitch_id {n : ℕ} {σ : Equiv.Perm (Fin n)} : IsSwitch σ (1 : Equiv.Perm (Fin n)) := by
…
```
Mentions: Usa2018P6.IsSwitch
lemma Usa2018P6.Perm_mul_self_eq_one_of_involutive An involution squares to one line 916 source
Source documentation
An involution squares to one.

standard axioms: Quot.sound what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Eq, HMul.hMul, OfNat.ofNat
Proof uses: Equiv.Perm.ext, Fin.ext, id, congrArg
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma Perm_mul_self_eq_one_of_involutive {n : ℕ} {ψ : Equiv.Perm (Fin n)}
    (h : Function.Involutive ψ) : ψ * ψ = 1 := by
…
```
Mentions: h
theorem Usa2018P6.card_switch_eq_one_of_fantastic A fantastic vertex admits only the trivial switching involution line 923 source
Source documentation
A fantastic vertex admits only the trivial switching involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Usa2018P6.Fantastic, Eq, Fintype.card, Subtype, Usa2018P6.IsSwitch, OfNat.ofNat
Proof uses: Iff.mpr, Equiv.Perm.ext_iff, dite, Membership.mem, Finset, Usa2018P6.nums, Rat, Usa2018P6.label, And.right, Not, Function.Involutive, And, Usa2018P6.switch_mapsTo_nums, Eq.mpr, id, congrArg, of_eq_true, eq_self, And.left, LE.le and 11 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem card_switch_eq_one_of_fantastic {n : ℕ} {σ : Equiv.Perm (Fin n)}
    (hf : Fantastic σ) : Fintype.card {φ : Equiv.Perm (Fin n) // IsSwitch σ φ} = 1 := by
…
```
Mentions: Usa2018P6.Fantastic, Usa2018P6.IsSwitch
lemma Usa2018P6.conj_isSwitch Conjugating a switching involution by the swap of two equal-labelled numerators yields a switching involution line 947 source
Source documentation
Conjugating a switching involution by the swap of two equal-labelled numerators yields a switching involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, Usa2018P6.IsSwitch, HMul.hMul, Equiv.swap
Proof uses: Eq.mpr, id, congrArg, rfl, Equiv.swap_apply_left, Equiv.swap_apply_right, Ne, Equiv.swap_apply_of_ne_of_ne, Function.Involutive, Equiv.swap_apply_self, Iff, dite, iff_of_true, Not, Iff.rfl, Eq.symm, Eq.refl, And.intro, And, And.left and 4 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma conj_isSwitch {n : ℕ} {σ : Equiv.Perm (Fin n)}
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (hab : label σ a = label σ b)
    {φ : Equiv.Perm (Fin n)} (hφ : IsSwitch σ φ) :
    IsSwitch σ (Equiv.swap a b * φ * Equiv.swap a b) := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.label, Usa2018P6.IsSwitch
def Usa2018P6.rho The involution obtained from σ by removing the two edges through a and b line 998 source
Source documentation
The involution obtained from σ by removing the two edges through a and b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin
Proof uses: HMul.hMul, Equiv.swap
6 instances, coercions and auxiliary constants left out.
```
def rho {n : ℕ} (σ : Equiv.Perm (Fin n)) (a b : Fin n) : Equiv.Perm (Fin n) :=
…
```
lemma Usa2018P6.rho_apply_a line 1001 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Eq, Usa2018P6.rho
Proof uses: Usa2018P6.denom_not_mem_nums, Eq.rec, Eq.symm, Equiv.injective, id, Eq.mpr, Equiv.swap, congrArg, Equiv.swap_apply_of_ne_of_ne, Equiv.swap_apply_right, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.rho_apply_σa line 1009 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Eq, Usa2018P6.rho
Proof uses: Usa2018P6.denom_not_mem_nums, Eq.rec, id, Eq.mpr, Equiv.swap, congrArg, Equiv.swap_apply_of_ne_of_ne, Equiv.swap_apply_left, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.rho_apply_b line 1016 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Eq, Usa2018P6.rho
Proof uses: Usa2018P6.denom_not_mem_nums, Eq.rec, id, Eq.mpr, Equiv.swap, congrArg, Equiv.swap_apply_right, Equiv.swap_apply_of_ne_of_ne, Ne.symm, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.rho_apply_σb line 1023 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Eq, Usa2018P6.rho
Proof uses: Usa2018P6.denom_not_mem_nums, Eq.rec, Eq.symm, Ne.symm, Equiv.injective, id, Eq.mpr, Equiv.swap, congrArg, Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.rho_apply_of_not_mem line 1031 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, And, Ne, Eq, Usa2018P6.rho
Proof uses: And.right, Eq.trans, Eq.symm, congrArg, And.left, Equiv.injective, id, Eq.mpr, Equiv.swap, Equiv.swap_apply_of_ne_of_ne, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.rho_involutive line 1041 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Usa2018P6.rho
Proof uses: dite, Eq, Or, Eq.mpr, id, congrArg, Usa2018P6.rho_apply_a, Eq.refl, Usa2018P6.rho_apply_σa, Eq.symm, Usa2018P6.rho_apply_b, Usa2018P6.rho_apply_σb, Not, Usa2018P6.rho_apply_of_not_mem, Eq.mp, And, Eq.trans, And.intro, And.left, And.right and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.not_mem_four_of_mem_nums_rho line 1065 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Usa2018P6.rho, And
Proof uses: LT.lt, Iff.mp, Usa2018P6.mem_nums_iff, And.intro, Eq, False, absurd, Eq.mp, congrArg, Usa2018P6.rho_apply_a, lt_irrefl, Usa2018P6.rho_apply_σa, Eq.symm, Usa2018P6.rho_apply_b, Usa2018P6.rho_apply_σb
14 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.nums_rho line 1081 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Eq, Usa2018P6.rho, Finset.filter, And
Proof uses: Finset.ext, Eq.mpr, Iff, LT.lt, id, congr, congrArg, Eq.trans, congrFun', Iff.intro, Usa2018P6.not_mem_four_of_mem_nums_rho, Iff.mpr, Usa2018P6.mem_nums_iff, And.intro, Eq.mp, Usa2018P6.rho_apply_of_not_mem, And.left, And.right, Usa2018P6.denom_not_mem_nums, Eq.rec
21 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.label_rho line 1101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Usa2018P6.rho, Eq, Rat, Usa2018P6.label
Proof uses: And, Usa2018P6.not_mem_four_of_mem_nums_rho, id, Eq.mpr, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, congrArg, Usa2018P6.rho_apply_of_not_mem, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa2018P6.permOfInvolutive Package an involutive function as a permutation line 1112 source
Source documentation
Package an involutive function as a permutation.

no axioms what this means
Statement uses: Function.Involutive, Equiv.Perm
Proof uses: Equiv.mk
```
def permOfInvolutive {α : Type*} (f : α → α) (hf : Function.Involutive f) : Equiv.Perm α where
…
```
Mentions: f
lemma Usa2018P6.permOfInvolutive_apply line 1119 source
standard axioms: Quot.sound what this means
Statement uses: Function.Involutive, Eq, Equiv.Perm, Usa2018P6.permOfInvolutive
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Usa2018P6.fixed_perm_ab If c * ψ = ψ * c for c = swap a b, then ψ preserves the pair {a, b} line 1123 source
Source documentation
If c * ψ = ψ * c for c = swap a b, then ψ preserves the pair {a, b}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, Ne, Usa2018P6.IsSwitch, HMul.hMul, Equiv.swap, And, Insert.insert, Singleton.singleton
Proof uses: Equiv.swap_apply_left, Equiv.Perm.mul_apply, Eq.symm, Eq.mp, congrArg, And.intro, Decidable.byContradiction, Not, Eq.mpr, id, Equiv.swap_apply_of_ne_of_ne, And.left, Eq.trans, Or, And.right, Eq.refl, Equiv.injective, Equiv.swap_apply_right
24 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma fixed_perm_ab {n : ℕ} {σ ψ : Equiv.Perm (Fin n)}
    {a b : Fin n} (_ha : a ∈ nums σ) (_hb : b ∈ nums σ) (_hab : label σ a = label σ b)
    (hne : a ≠ b)
    (_hψ : IsSwitch σ ψ) (hcomm : Equiv.swap a b * ψ = ψ * Equiv.swap a b) :
    ψ a ∈ ({a, b} : Finset (Fin n)) ∧ ψ b ∈ ({a, b} : Finset (Fin n)) := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.label, Usa2018P6.IsSwitch
lemma Usa2018P6.perm_compl_of_perm_ab A permutation preserving a two-element set also preserves its complement line 1151 source
Source documentation
A permutation preserving a two-element set also preserves its complement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Membership.mem, Finset, Insert.insert, Singleton.singleton, Not
Proof uses: LE.le, Finset.image, Iff.mpr, Finset.image_subset_iff, Eq, Finset.card, Eq.mpr, id, congrArg, Equiv, Finset.card_image_of_injective, Equiv.injective, Eq.refl, Finset.eq_of_subset_of_card_le, le_refl, And, Exists, False, Iff.mp, Finset.mem_image and 3 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma perm_compl_of_perm_ab {n : ℕ} {ψ : Equiv.Perm (Fin n)} {a b : Fin n}
    (h : ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n)))
    (y : Fin n) (hy : y ∉ ({a, b} : Finset (Fin n))) :
    ψ y ∉ ({a, b} : Finset (Fin n)) := by
…
```
Mentions: h
def Usa2018P6.restrictAb The restriction of an involution to a preserved pair {a, b} line 1166 source
Source documentation
The restriction of an involution to a preserved pair {a, b}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton
Proof uses: Usa2018P6.permOfInvolutive, ite
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
def restrictAb {n : ℕ} {ψ : Equiv.Perm (Fin n)} (hψ : Function.Involutive ψ)
    {a b : Fin n} (h : ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n))) :
    Equiv.Perm (Fin n) :=
…
```
Mentions: h
lemma Usa2018P6.restrictAb_apply_of_mem line 1178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Eq, Usa2018P6.restrictAb
Proof uses: id, Eq.mpr, Usa2018P6.permOfInvolutive, ite, congrArg, Usa2018P6.permOfInvolutive_apply, ite_eq_left, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.restrictAb_apply_of_not_mem line 1186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Not, Eq, Usa2018P6.restrictAb
Proof uses: id, Eq.mpr, Usa2018P6.permOfInvolutive, ite, congrArg, Usa2018P6.permOfInvolutive_apply, ite_eq_right, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.restrictAb_involutive line 1194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Usa2018P6.restrictAb
Proof uses: dite, Eq, Eq.mpr, id, congrArg, Usa2018P6.restrictAb_apply_of_mem, Eq.refl, Not, Usa2018P6.restrictAb_apply_of_not_mem
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def Usa2018P6.restrictCompl The restriction of an involution to the complement of a preserved pair {a, b} line 1204 source
Source documentation
The restriction of an involution to the complement of a preserved pair {a, b}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton
Proof uses: Usa2018P6.permOfInvolutive, ite
18 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
def restrictCompl {n : ℕ} {ψ : Equiv.Perm (Fin n)} (hψ : Function.Involutive ψ)
    {a b : Fin n} (h : ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n))) :
    Equiv.Perm (Fin n) :=
…
```
Mentions: h
lemma Usa2018P6.restrictCompl_apply_of_mem line 1216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Eq, Usa2018P6.restrictCompl
Proof uses: id, Eq.mpr, Usa2018P6.permOfInvolutive, ite, congrArg, Usa2018P6.permOfInvolutive_apply, ite_eq_left, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.restrictCompl_apply_of_not_mem line 1224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Not, Eq, Usa2018P6.restrictCompl
Proof uses: id, Eq.mpr, Usa2018P6.permOfInvolutive, ite, congrArg, Usa2018P6.permOfInvolutive_apply, ite_eq_right, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.restrictCompl_involutive line 1232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Usa2018P6.restrictCompl
Proof uses: dite, Eq, Eq.mpr, id, congrArg, Usa2018P6.restrictCompl_apply_of_mem, Eq.refl, Not, Usa2018P6.restrictCompl_apply_of_not_mem, Usa2018P6.perm_compl_of_perm_ab
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2018P6.mul_restrictAb_restrictCompl An involution decomposes as the product of its two restrictions line 1243 source
Source documentation
An involution decomposes as the product of its two restrictions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Eq, HMul.hMul, Usa2018P6.restrictAb, Usa2018P6.restrictCompl
Proof uses: Iff.mpr, Equiv.Perm.ext_iff, Eq.mpr, id, congrArg, Equiv.Perm.mul_apply, dite, Usa2018P6.restrictCompl_apply_of_mem, Usa2018P6.restrictAb_apply_of_mem, Eq.refl, Not, Usa2018P6.restrictCompl_apply_of_not_mem, Usa2018P6.restrictAb_apply_of_not_mem, Usa2018P6.perm_compl_of_perm_ab
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma mul_restrictAb_restrictCompl {n : ℕ} {ψ : Equiv.Perm (Fin n)}
    (hψ : Function.Involutive ψ) {a b : Fin n}
    (h : ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n))) :
    restrictAb hψ h * restrictCompl hψ h = ψ := by
…
```
Mentions: h, Usa2018P6.restrictAb, Usa2018P6.restrictCompl
lemma Usa2018P6.restrictAb_eq_one_or_c On a preserved pair {a, b}, an involution is either the identity or the swap line 1256 source
Source documentation
On a preserved pair {a, b}, an involution is either the identity or the swap.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Ne, Function.Involutive, Membership.mem, Finset, Insert.insert, Singleton.singleton, Or, Eq, Usa2018P6.restrictAb, OfNat.ofNat, Equiv.swap
Proof uses: Finset.mem_insert_self, of_eq_true, Eq.trans, True, congrArg, eq_self, or_true, Eq.mp, Or.inl, absurd, Eq.symm, Equiv.injective, Equiv, Or.inr, Eq.refl, Iff.mpr, Equiv.Perm.ext_iff, dite, Eq.mpr, id and 11 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma restrictAb_eq_one_or_c {n : ℕ} {ψ : Equiv.Perm (Fin n)}
    {a b : Fin n} (hne : a ≠ b) (hψ : Function.Involutive ψ)
    (h : ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n))) :
    restrictAb hψ h = 1 ∨ restrictAb hψ h = Equiv.swap a b := by
…
```
Mentions: h, Usa2018P6.restrictAb
lemma Usa2018P6.isSwitch_rho_of_restrictCompl The complement restriction of a fixed switching involution is a switching involution of the reduced vertex ρ line 1310 source
Source documentation
The complement restriction of a fixed switching involution is a switching involution of the reduced vertex ρ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, Ne, Usa2018P6.IsSwitch, Insert.insert, Singleton.singleton, Usa2018P6.rho, Usa2018P6.restrictCompl, And.left, And, Not
Proof uses: And.intro, Usa2018P6.restrictCompl_involutive, dite, Usa2018P6.restrictCompl_apply_of_mem, Eq.mpr, id, congrArg, Usa2018P6.restrictCompl_apply_of_not_mem, Eq.mp, Finset.filter, Usa2018P6.nums_rho, Iff.mpr, Finset.mem_filter, Eq.trans, Or, And.right, False, Or.inl, Or.inr, Eq.refl and 4 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma isSwitch_rho_of_restrictCompl {n : ℕ} {σ ψ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ)
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (_hab : label σ a = label σ b)
    (hne : a ≠ b) (hψ : IsSwitch σ ψ)
    (h : ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n))) :
    IsSwitch (rho σ a b) (restrictCompl hψ.1 h) := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.label, Usa2018P6.IsSwitch, h, Usa2018P6.rho, Usa2018P6.restrictCompl
lemma Usa2018P6.isSwitch_mul The product of a permutation of {a, b} (identity or swap) with a switching involution of the reduced vertex ρ is a switching involution of σ line 1352 source
Source documentation
The product of a permutation of {a, b} (identity or swap) with a switching involution of the reduced vertex ρ is a switching involution of σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, Ne, Or, OfNat.ofNat, Equiv.swap, Usa2018P6.IsSwitch, Usa2018P6.rho, HMul.hMul
Proof uses: Equiv.swap_apply_left, Equiv.swap_apply_right, Insert.insert, Singleton.singleton, Eq.mp, Eq.trans, congrArg, Or.inl, Eq.rec, Eq.symm, Or.inr, Eq.refl, And.left, Not, And.right, And, False, Finset.filter, Usa2018P6.nums_rho, Eq.mpr and 20 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 109 steps
Open to load the checked before-and-after goal states.
```
lemma isSwitch_mul {n : ℕ} {σ : Equiv.Perm (Fin n)} (hσ : Function.Involutive σ)
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (hab : label σ a = label σ b)
    (hne : a ≠ b)
    {ψ₀ ψ₁ : Equiv.Perm (Fin n)} (hψ₀ : ψ₀ = 1 ∨ ψ₀ = Equiv.swap a b)
    (hψ₁ : IsSwitch (rho σ a b) ψ₁) :
    IsSwitch σ (ψ₀ * ψ₁) := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.label, Usa2018P6.IsSwitch, Usa2018P6.rho
lemma Usa2018P6.switch_rho_fix_of_mem_ab A switching involution of the reduced vertex fixes both a and b line 1453 source
Source documentation
A switching involution of the reduced vertex fixes both a and b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Usa2018P6.IsSwitch, Usa2018P6.rho, Insert.insert, Singleton.singleton, Eq
Proof uses: And.left, Not, Rat, Usa2018P6.label, And.right, And, Iff.mp, Finset.filter, Finset.mem_filter, Eq.mp, congrArg, Usa2018P6.nums_rho, Or, Eq.trans, False, Or.inl, Or.inr, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma switch_rho_fix_of_mem_ab {n : ℕ} {σ ψ₁ : Equiv.Perm (Fin n)} (hσ : Function.Involutive σ)
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (hne : a ≠ b)
    (hψ₁ : IsSwitch (rho σ a b) ψ₁) {x : Fin n} (hx : x ∈ ({a, b} : Finset (Fin n))) :
    ψ₁ x = x := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.IsSwitch, Usa2018P6.rho
lemma Usa2018P6.perm_ab_of_fixed A fixed switching involution preserves the pair {a, b} (bundled form) line 1467 source
Source documentation
A fixed switching involution preserves the pair {a, b} (bundled form).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, Ne, Usa2018P6.IsSwitch, HMul.hMul, Equiv.swap, Insert.insert, Singleton.singleton
Proof uses: And, Usa2018P6.fixed_perm_ab, Or, Eq.mp, Eq.trans, congrArg, Or.inl, And.left, Or.inr, And.right, Eq.refl
24 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma perm_ab_of_fixed {n : ℕ} {σ ψ : Equiv.Perm (Fin n)}
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (hab : label σ a = label σ b)
    (hne : a ≠ b) (hψ : IsSwitch σ ψ) (hcomm : Equiv.swap a b * ψ = ψ * Equiv.swap a b) :
    ∀ y ∈ ({a, b} : Finset (Fin n)), ψ y ∈ ({a, b} : Finset (Fin n)) := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.label, Usa2018P6.IsSwitch
lemma Usa2018P6.commute_c_of_mem The product ψ₀ * ψ₁ commutes with swap a b when ψ₀ ∈ {1, swap a b} and ψ₁ is a switching involution of the reduced vertex line 1480 source
Source documentation
The product ψ₀ * ψ₁ commutes with swap a b when ψ₀ ∈ {1, swap a b} and ψ₁ is a switching involution of the reduced vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Ne, Or, Eq, OfNat.ofNat, Equiv.swap, Usa2018P6.IsSwitch, Usa2018P6.rho, HMul.hMul
Proof uses: Commute, Or.inl, Eq.mpr, id, congrArg, Commute.one_right, Or.inr, Commute.refl, Eq.refl, Equiv.Perm.Disjoint.commute, dite, Insert.insert, Singleton.singleton, Usa2018P6.switch_rho_fix_of_mem_ab, Not, Equiv.swap_apply_of_ne_of_ne, And.left, Eq.mp, And, Eq.trans and 5 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma commute_c_of_mem {n : ℕ} {σ : Equiv.Perm (Fin n)} (hσ : Function.Involutive σ)
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (hne : a ≠ b)
    {ψ₀ ψ₁ : Equiv.Perm (Fin n)} (hψ₀ : ψ₀ = 1 ∨ ψ₀ = Equiv.swap a b)
    (hψ₁ : IsSwitch (rho σ a b) ψ₁) :
    Equiv.swap a b * (ψ₀ * ψ₁) = (ψ₀ * ψ₁) * Equiv.swap a b := by
…
```
Mentions: Usa2018P6.nums, Usa2018P6.IsSwitch, Usa2018P6.rho
def Usa2018P6.fixedDecompEquiv The fixed points of the conjugation involution decompose as a choice on {a, b} (identity or swap) times a switching involution of the reduced vertex line 1505 source
Source documentation
The fixed points of the conjugation involution decompose as a choice on {a, b} (identity or swap) times a switching involution of the reduced vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Membership.mem, Finset, Usa2018P6.nums, Eq, Rat, Usa2018P6.label, Ne, Equiv, Subtype, And, Usa2018P6.IsSwitch, HMul.hMul, Equiv.swap, Prod, Or, OfNat.ofNat and 1 more
Proof uses: Equiv.mk, Prod.mk, Subtype.mk, Usa2018P6.restrictAb, Usa2018P6.restrictCompl, Prod.fst, Prod.snd
28 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
def fixedDecompEquiv {n : ℕ} {σ : Equiv.Perm (Fin n)} (hσ : Function.Involutive σ)
    {a b : Fin n} (ha : a ∈ nums σ) (hb : b ∈ nums σ) (hab : label σ a = label σ b)
    (hne : a ≠ b) :
    {ψ : Equiv.Perm (Fin n) // IsSwitch σ ψ ∧ Equiv.swap a b * ψ = ψ * Equiv.swap a b} ≃
      {ψ₀ : Equiv.Perm (Fin n) // ψ₀ = 1 ∨ ψ₀ = Equiv.swap a b} ×
        {ψ₁ : Equiv.Perm (Fin n) // IsSwitch (rho σ a b) ψ₁} where
…
```
Mentions: Usa2018P6.nums, Usa2018P6.label, Usa2018P6.IsSwitch, Usa2018P6.rho
theorem Usa2018P6.even_card_switch_of_not_fantastic A non-fantastic vertex admits an even number of switching involutions line 1580 source
Source documentation
A non-fantastic vertex admits an even number of switching involutions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Function.Involutive, Not, Usa2018P6.Fantastic, Even, Fintype.card, Subtype, Usa2018P6.IsSwitch
Proof uses: And, Membership.mem, Finset, Usa2018P6.nums, Exists, Eq, Rat, Usa2018P6.label, Ne, Eq.mp, Set, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, HMul.hMul, Equiv.swap, OfNat.ofNat, Usa2018P6.Perm_mul_self_eq_one_of_involutive, Equiv.swap_apply_self and 41 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
theorem even_card_switch_of_not_fantastic {n : ℕ} {σ : Equiv.Perm (Fin n)}
    (hσ : Function.Involutive σ) (hf : ¬ Fantastic σ) :
    Even (Fintype.card {φ : Equiv.Perm (Fin n) // IsSwitch σ φ}) := by
…
```
Mentions: Usa2018P6.Fantastic, Usa2018P6.IsSwitch
instance Usa2018P6.usa2018p6_aux.decInvol Decidability of being an involution on Fin n line 1646 source
Source documentation
Decidability of being an involution on Fin n.

no axioms what this means
Statement uses: Nat, DecidablePred, Fin, Function.Involutive
1 instances, coercions and auxiliary constants left out.
```
instance decInvol {n : ℕ} : DecidablePred (Function.Involutive (α := Fin n)) := fun σ =>
…
```
def Usa2018P6.usa2018p6_aux.fpfSubtype Fixed-point-free involutions of Fin n line 1650 source
Source documentation
Fixed-point-free involutions of Fin n.

standard axioms: Quot.sound what this means
Statement uses: Nat
Proof uses: Subtype, Equiv.Perm, Fin, And, Function.Involutive, Ne
3 instances, coercions and auxiliary constants left out.
```
def fpfSubtype (n : ℕ) :=
…
```
def Usa2018P6.usa2018p6_aux.vtxSubtype Involutions of Fin n with at most one fixed point line 1654 source
Source documentation
Involutions of Fin n with at most one fixed point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Subtype, Equiv.Perm, Fin, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def vtxSubtype (n : ℕ) :=
…
```
instance Usa2018P6.usa2018p6_aux.(instance at line 1658) line 1658 source
instance Usa2018P6.usa2018p6_aux.(instance at line 1661) line 1661 source
def Usa2018P6.usa2018p6_aux.fcard The number of fixed-point-free involutions of Fin n line 1665 source
Source documentation
The number of fixed-point-free involutions of Fin n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fintype.card, Usa2018P6.usa2018p6_aux.fpfSubtype
1 instances, coercions and auxiliary constants left out.
```
noncomputable def fcard (n : ℕ) : ℕ := Fintype.card (fpfSubtype n)
```
Mentions: Usa2018P6.usa2018p6_aux.fpfSubtype
def Usa2018P6.usa2018p6_aux.vcard The number of involutions of Fin n with at most one fixed point line 1668 source
Source documentation
The number of involutions of Fin n with at most one fixed point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fintype.card, Usa2018P6.usa2018p6_aux.vtxSubtype
1 instances, coercions and auxiliary constants left out.
```
noncomputable def vcard (n : ℕ) : ℕ := Fintype.card (vtxSubtype n)
```
Mentions: Usa2018P6.usa2018p6_aux.vtxSubtype
theorem Usa2018P6.usa2018p6_aux.decomposeFin_fst line 1672 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Nat.succ, Prod.fst, Equiv, Prod, Equiv.Perm.decomposeFin
Proof uses: Eq.mpr, Equiv.symm, Prod.mk, Prod.snd, id, congrArg, Eq.symm, Equiv.Perm.decomposeFin_symm_apply_zero, Prod.mk.eta, Equiv.symm_apply_apply, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Usa2018P6.usa2018p6_aux.partner The partner of 0 under a permutation that moves 0, seen as an element of Fin (n + 1) via Fin.pred line 1679 source
Source documentation
The partner of 0 under a permutation that moves 0, seen as an element of Fin (n + 1) via Fin.pred.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Ne
Proof uses: Fin.pred, Prod.fst, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
noncomputable def partner {n : ℕ} (σ : Equiv.Perm (Fin (n + 2))) (_h0 : σ 0 ≠ 0) :
    Fin (n + 1) :=
…
```
theorem Usa2018P6.usa2018p6_aux.partner_succ line 1685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Eq, Fin.succ, Usa2018P6.usa2018p6_aux.partner
Proof uses: id, Eq.mpr, Fin.pred, Prod.fst, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin, congrArg, Fin.succ_pred, Usa2018P6.usa2018p6_aux.decomposeFin_fst, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_partner line 1690 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Eq, Equiv, Prod, Nat.succ, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Fin.succ, Usa2018P6.usa2018p6_aux.partner, Prod.snd
Proof uses: Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.partner_succ, Prod.fst, Eq.symm, Usa2018P6.usa2018p6_aux.decomposeFin_fst, Prod.mk.eta, Equiv.symm_apply_apply
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_zero line 1695 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Equiv, Prod, Nat.succ, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Prod.snd
Proof uses: Prod.fst, Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.decomposeFin_fst, Eq.symm, Prod.mk.eta, Equiv.symm_apply_apply
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.partner_symm_succ The partner of 0 under decomposeFin.symm (j.succ, e) is j itself line 1704 source
Source documentation
The partner of 0 under decomposeFin.symm (j.succ, e) is j itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Ne, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Fin.succ, Eq, Usa2018P6.usa2018p6_aux.partner
Proof uses: Usa2018P6.usa2018p6_aux.partner_succ, Iff.mp, Fin.succ_inj, Eq.mp, congrArg, Equiv.Perm.decomposeFin_symm_apply_zero
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem partner_symm_succ {n : ℕ} (j : Fin (n + 1)) (e : Equiv.Perm (Fin (n + 1)))
    (h0 : (Equiv.Perm.decomposeFin.symm (j.succ, e)) 0 ≠ 0) :
    partner (Equiv.Perm.decomposeFin.symm (j.succ, e)) h0 = j := by
…
```
Mentions: Usa2018P6.usa2018p6_aux.partner
theorem Usa2018P6.usa2018p6_aux.involutive_symm_succ Involutivity of decomposeFin.symm (j.succ, e) corresponds to involutivity of e together with e j = j line 1715 source
Source documentation
Involutivity of decomposeFin.symm (j.succ, e) corresponds to involutivity of e together with e j = j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Iff, Function.Involutive, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Fin.succ, And, Eq
Proof uses: Equiv.swap, dite, absurd, Eq.mp, congrArg, Equiv.swap_apply_left, Fin.succ_ne_zero, Eq.symm, Not, Equiv.swap_apply_of_ne_of_ne, Iff.intro, Iff.mp, Fin.succ_inj, Equiv.Perm.decomposeFin_symm_apply_succ, Equiv.Perm.decomposeFin_symm_apply_zero, And.intro, Eq.mpr, id, Equiv.swap_apply_right, Eq.refl and 4 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
theorem involutive_symm_succ {n : ℕ} (j : Fin (n + 1)) (e : Equiv.Perm (Fin (n + 1))) :
    Function.Involutive (Equiv.Perm.decomposeFin.symm (j.succ, e)) ↔
      Function.Involutive e ∧ e j = j := by
…
```
theorem Usa2018P6.usa2018p6_aux.fpf_symm_succ decomposeFin.symm (j.succ, e) is fixed-point-free iff e has no fixed point other than j line 1780 source
Source documentation
decomposeFin.symm (j.succ, e) is fixed-point-free iff e has no fixed point other than j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Function.Involutive, Eq, Iff, Ne, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Fin.succ
Proof uses: Iff.intro, Equiv.swap, False, Eq.trans, Eq.symm, Eq.mp, congrArg, Equiv.Perm.decomposeFin_symm_apply_succ, Equiv.swap_apply_of_ne_of_ne, Fin.succ_ne_zero, Iff.mp, Fin.succ_inj, Fin.cases, Eq.mpr, id, Equiv.Perm.decomposeFin_symm_apply_zero, dite, Equiv.swap_apply_right, Ne.symm, Not
17 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
theorem fpf_symm_succ {n : ℕ} (j : Fin (n + 1)) (e : Equiv.Perm (Fin (n + 1)))
    (he : Function.Involutive e) (hej : e j = j) :
    (∀ y : Fin (n + 2), Equiv.Perm.decomposeFin.symm (j.succ, e) y ≠ y) ↔
      ∀ x : Fin (n + 1), x ≠ j → e x ≠ x := by
…
```
theorem Usa2018P6.usa2018p6_aux.card_fp_symm_succ The fixed points of decomposeFin.symm (j.succ, e) are in bijection with the fixed points of e different from j line 1814 source
Source documentation
The fixed points of decomposeFin.symm (j.succ, e) are in bijection with the fixed points of e different from j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Function.Involutive, Eq, Finset.card, Finset.filter, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Fin.succ, Finset.univ, And, Ne
Proof uses: Eq.symm, Finset.card_bij, Membership.mem, Finset, Eq.mpr, id, congrArg, propext, Finset.mem_filter, Eq.mp, And.intro, Finset.mem_univ, Equiv.swap, Equiv.Perm.decomposeFin_symm_apply_succ, Equiv.swap_apply_of_ne_of_ne, Fin.succ_ne_zero, Iff.mp, Fin.succ_inj, Eq.refl, Exists and 11 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
theorem card_fp_symm_succ {n : ℕ} (j : Fin (n + 1)) (e : Equiv.Perm (Fin (n + 1)))
    (he : Function.Involutive e) (hej : e j = j) :
    (Finset.univ.filter fun y : Fin (n + 2) =>
        Equiv.Perm.decomposeFin.symm (j.succ, e) y = y).card =
      (Finset.univ.filter fun x : Fin (n + 1) => x ≠ j ∧ e x = x).card := by
…
```
theorem Usa2018P6.usa2018p6_aux.involutive_symm_zero Involutivity of decomposeFin.symm (0, e) corresponds to involutivity of e line 1852 source
Source documentation
Involutivity of decomposeFin.symm (0, e) corresponds to involutivity of e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Iff, Function.Involutive, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk
Proof uses: Iff.intro, Eq, Fin.succ, Eq.mp, congrArg, propext, Fin.succ_inj, Equiv.refl, Equiv.refl_apply, Equiv.swap, Equiv.swap_self, Equiv.Perm.decomposeFin_symm_apply_succ, Fin.cases, Eq.mpr, id, Equiv.Perm.decomposeFin_symm_apply_zero, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem involutive_symm_zero {n : ℕ} (e : Equiv.Perm (Fin (n + 1))) :
    Function.Involutive (Equiv.Perm.decomposeFin.symm (0, e)) ↔ Function.Involutive e := by
…
```
theorem Usa2018P6.usa2018p6_aux.fp_symm_zero The fixed points of decomposeFin.symm (0, e) are 0 together with the successors of fixed points of e line 1870 source
Source documentation
The fixed points of decomposeFin.symm (0, e) are 0 together with the successors of fixed points of e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Iff, Eq, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Or, Exists, And, Fin.succ
Proof uses: Fin.cases, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', Equiv.Perm.decomposeFin_symm_apply_zero, eq_self, true_or, iff_self, Eq.mpr, Equiv.swap, id, Equiv.Perm.decomposeFin_symm_apply_succ, Equiv.refl, Equiv.swap_self, Equiv.refl_apply, Iff.intro, Or.inr and 10 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem fp_symm_zero {n : ℕ} (e : Equiv.Perm (Fin (n + 1))) (y : Fin (n + 2)) :
    Equiv.Perm.decomposeFin.symm (0, e) y = y ↔
      y = 0 ∨ ∃ x : Fin (n + 1), y = x.succ ∧ e x = x := by
…
```
theorem Usa2018P6.usa2018p6_aux.card_le_one_symm_zero_iff decomposeFin.symm (0, e) has at most one fixed point iff e is fixed-point-free line 1887 source
Source documentation
decomposeFin.symm (0, e) has at most one fixed point iff e is fixed-point-free.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Iff, LE.le, Finset.card, Finset.filter, Eq, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Finset.univ, Ne
Proof uses: Iff.intro, Membership.mem, Finset, Eq.mpr, And, id, congrArg, propext, Finset.mem_filter, And.intro, Finset.mem_univ, Iff.mpr, Or, Exists, Fin.succ, Usa2018P6.usa2018p6_aux.fp_symm_zero, Or.inl, rfl, Or.inr, Exists.intro and 16 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
theorem card_le_one_symm_zero_iff {n : ℕ} (e : Equiv.Perm (Fin (n + 1))) :
    (Finset.univ.filter fun y : Fin (n + 2) =>
        Equiv.Perm.decomposeFin.symm (0, e) y = y).card ≤ 1 ↔
      ∀ x : Fin (n + 1), e x ≠ x := by
…
```
def Usa2018P6.usa2018p6_aux.restrictPerm Restriction of a permutation fixing j to the complement of j, transported to Fin n along finSuccAboveEquiv line 1935 source
Source documentation
Restriction of a permutation fixing j to the complement of j, transported to Fin n along finSuccAboveEquiv.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq
Proof uses: Equiv, Subtype, Ne, Equiv.permCongr, Equiv.symm, finSuccAboveEquiv, Equiv.Perm.subtypePerm
13 instances, coercions and auxiliary constants left out.
```
noncomputable def restrictPerm {n : ℕ} {j : Fin (n + 1)} (e : Equiv.Perm (Fin (n + 1)))
    (hej : e j = j) : Equiv.Perm (Fin n) :=
…
```
theorem Usa2018P6.usa2018p6_aux.restrictPerm_apply line 1941 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Ne, Equiv, Subtype, finSuccAboveEquiv, Usa2018P6.usa2018p6_aux.restrictPerm
Proof uses: of_eq_true, Not, Eq.trans, True, congrFun', congrArg, Subtype.mk, Iff.mpr, Subtype.property, Equiv.apply_symm_apply, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.restrictPerm_involutive line 1946 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Function.Involutive, Eq, Usa2018P6.usa2018p6_aux.restrictPerm
Proof uses: Equiv.injective, Subtype, Ne, finSuccAboveEquiv, Subtype.ext, Equiv, Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.restrictPerm_apply, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.restrictPerm_fix_iff line 1954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Iff, Usa2018P6.usa2018p6_aux.restrictPerm, Ne, Equiv, Subtype, finSuccAboveEquiv
Proof uses: Iff.intro, congrArg, Usa2018P6.usa2018p6_aux.restrictPerm_apply, Eq.symm, Eq.mp, Equiv.injective, Subtype.ext, Eq.mpr, id
14 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.card_fp_restrictPerm The fixed points of restrictPerm e hej are in bijection with the fixed points of e different from j line 1972 source
Source documentation
The fixed points of restrictPerm e hej are in bijection with the fixed points of e different from j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Finset.card, Finset.filter, Usa2018P6.usa2018p6_aux.restrictPerm, Finset.univ, And, Ne
Proof uses: Finset.card_bij, Membership.mem, Finset, Equiv, Subtype, finSuccAboveEquiv, Eq.mpr, id, congrArg, propext, Finset.mem_filter, And.intro, Finset.mem_univ, Subtype.property, Iff.mp, Usa2018P6.usa2018p6_aux.restrictPerm_fix_iff, And.right, Eq.mp, Equiv.injective, Subtype.ext and 5 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem card_fp_restrictPerm {n : ℕ} {j : Fin (n + 1)} (e : Equiv.Perm (Fin (n + 1)))
    (hej : e j = j) :
    (Finset.univ.filter fun y : Fin n => restrictPerm e hej y = y).card =
      (Finset.univ.filter fun x : Fin (n + 1) => x ≠ j ∧ e x = x).card := by
…
```
Mentions: Usa2018P6.usa2018p6_aux.restrictPerm
theorem Usa2018P6.usa2018p6_aux.fpf_restrictPerm line 1993 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Ne, Usa2018P6.usa2018p6_aux.restrictPerm
Proof uses: Equiv, Subtype, finSuccAboveEquiv, Subtype.property, Iff.mp, Usa2018P6.usa2018p6_aux.restrictPerm_fix_iff
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2018P6.usa2018p6_aux.extendPerm Extension of a permutation of Fin n to Fin (n + 1) fixing j, via the identification Fin n ≃ {x // x ≠ j} line 2003 source
Source documentation
Extension of a permutation of Fin n to Fin (n + 1) fixing j, via the identification Fin n ≃ {x // x ≠ j}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm
Proof uses: Equiv.trans, Sum, Subtype, Eq, Not, Equiv.symm, Equiv.sumCompl, Ne, Equiv.sumCongr, Equiv.refl, Equiv, Equiv.permCongr, finSuccAboveEquiv
10 instances, coercions and auxiliary constants left out.
```
noncomputable def extendPerm {n : ℕ} (j : Fin (n + 1)) (τ : Equiv.Perm (Fin n)) :
    Equiv.Perm (Fin (n + 1)) :=
…
```
theorem Usa2018P6.usa2018p6_aux.extendPerm_apply_self line 2009 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Usa2018P6.usa2018p6_aux.extendPerm
Proof uses: Sum, Subtype, Not, Equiv, Equiv.symm, Equiv.sumCompl, Sum.inl, Subtype.mk, rfl, Equiv.sumCompl_symm_apply_of_pos, of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.trans, Equiv.sumCongr, Equiv.refl, Ne, Equiv.permCongr and 3 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.extendPerm_apply_ne line 2015 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Ne, Eq, Usa2018P6.usa2018p6_aux.extendPerm, Equiv, Subtype, finSuccAboveEquiv, Equiv.symm, Subtype.mk
Proof uses: Sum, Not, Equiv.sumCompl, Sum.inr, Equiv.sumCompl_symm_apply_of_neg, of_eq_true, Eq.trans, True, congrFun', congrArg, Equiv.trans, Equiv.sumCongr, Equiv.refl, Equiv.permCongr, Equiv.sumCongr_apply, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.extendPerm_involutive line 2023 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Function.Involutive, Usa2018P6.usa2018p6_aux.extendPerm
Proof uses: dite, Eq, Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.extendPerm_apply_self, Eq.refl, Not, Ne, Equiv, Subtype, finSuccAboveEquiv, Equiv.symm, Subtype.mk, Usa2018P6.usa2018p6_aux.extendPerm_apply_ne, Subtype.property, Subtype.ext, rfl, Equiv.symm_apply_apply, Equiv.apply_symm_apply
14 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.extendPerm_fix_iff line 2037 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Ne, Iff, Eq, Usa2018P6.usa2018p6_aux.extendPerm, Equiv, Subtype, Equiv.symm, finSuccAboveEquiv, Subtype.mk
Proof uses: Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.extendPerm_apply_ne, Iff.intro, Equiv.injective, Equiv.apply_symm_apply, Subtype.ext
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.extendPerm_restrictPerm line 2051 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Usa2018P6.usa2018p6_aux.extendPerm, Usa2018P6.usa2018p6_aux.restrictPerm
Proof uses: Equiv.ext, dite, Equiv, Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.extendPerm_apply_self, Eq.refl, Not, Ne, Subtype, finSuccAboveEquiv, Equiv.symm, Subtype.mk, Usa2018P6.usa2018p6_aux.extendPerm_apply_ne, Usa2018P6.usa2018p6_aux.restrictPerm_apply, Equiv.apply_symm_apply
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.restrictPerm_extendPerm line 2059 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Eq, Usa2018P6.usa2018p6_aux.restrictPerm, Usa2018P6.usa2018p6_aux.extendPerm, Usa2018P6.usa2018p6_aux.extendPerm_apply_self
Proof uses: Equiv.ext, Equiv.injective, Subtype, Ne, finSuccAboveEquiv, Equiv, Subtype.ext, Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.restrictPerm_apply, Equiv.symm, Subtype.mk, Subtype.property, Usa2018P6.usa2018p6_aux.extendPerm_apply_ne, rfl, Equiv.symm_apply_apply, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.fpf_extendPerm line 2070 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Ne, Usa2018P6.usa2018p6_aux.extendPerm
Proof uses: Eq, Equiv, Subtype, Equiv.symm, finSuccAboveEquiv, Subtype.mk, Iff.mp, Usa2018P6.usa2018p6_aux.extendPerm_fix_iff
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.invol_decomposeFin_symm line 2077 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Function.Involutive, And, Prod.snd, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin, Eq, Usa2018P6.usa2018p6_aux.partner
Proof uses: Iff.mp, Equiv.symm, Prod.mk, Fin.succ, Usa2018P6.usa2018p6_aux.involutive_symm_succ, Eq.mp, congrArg, Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_partner
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.fpf_e line 2085 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Function.Involutive, Usa2018P6.usa2018p6_aux.partner, Prod.snd, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin
Proof uses: Iff.mp, Equiv.symm, Prod.mk, Fin.succ, Usa2018P6.usa2018p6_aux.fpf_symm_succ, And.left, Eq, Usa2018P6.usa2018p6_aux.invol_decomposeFin_symm, And.right, Eq.mp, congrArg, Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_partner
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.card_e_le_one line 2093 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Ne, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, Usa2018P6.usa2018p6_aux.restrictPerm, Usa2018P6.usa2018p6_aux.partner, Prod.snd, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin, And.right and 1 more
Proof uses: Eq.mp, And, congrArg, Eq.symm, Usa2018P6.usa2018p6_aux.card_fp_restrictPerm, Equiv.symm, Prod.mk, Fin.succ, Usa2018P6.usa2018p6_aux.card_fp_symm_succ, And.left, Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_partner
26 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.card_extend_le_one line 2106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, Equiv.Perm, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, Nat.succ, Equiv, Prod, Equiv.symm, Equiv.Perm.decomposeFin, Prod.mk, Fin.succ, Usa2018P6.usa2018p6_aux.extendPerm
Proof uses: And, Ne, Eq.mpr, Usa2018P6.usa2018p6_aux.restrictPerm, Usa2018P6.usa2018p6_aux.extendPerm_apply_self, id, congrArg, Eq.symm, Usa2018P6.usa2018p6_aux.card_fp_restrictPerm, Usa2018P6.usa2018p6_aux.restrictPerm_extendPerm, Eq.refl, Usa2018P6.usa2018p6_aux.card_fp_symm_succ, Usa2018P6.usa2018p6_aux.extendPerm_involutive
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.invol_e0 line 2117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Eq, Function.Involutive, Prod.snd, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin
Proof uses: Iff.mp, Equiv.symm, Prod.mk, Usa2018P6.usa2018p6_aux.involutive_symm_zero, Eq.mp, congrArg, Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_zero
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.fpf_e0 line 2123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, Eq, LE.le, Finset.card, Finset.filter, Finset.univ, Ne, Prod.snd, Nat.succ, Equiv, Prod, Equiv.Perm.decomposeFin
Proof uses: Iff.mp, Equiv.symm, Prod.mk, Usa2018P6.usa2018p6_aux.card_le_one_symm_zero_iff, Eq.mp, congrArg, Usa2018P6.usa2018p6_aux.decomposeFin_eq_symm_zero
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa2018P6.usa2018p6_aux.fpfDecomposeEquiv Fixed-point-free involutions of Fin (n + 2) are in bijection with pairs of an element j : Fin (n + 1) (the partner of 0) and a fixed-point-free involution of Fin n line 2135 source
Source documentation
Fixed-point-free involutions of Fin (n + 2) are in bijection with pairs of an element j : Fin (n + 1) (the partner of 0) and a fixed-point-free involution of Fin n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Usa2018P6.usa2018p6_aux.fpfSubtype, HAdd.hAdd, OfNat.ofNat, Prod, Fin
Proof uses: Equiv.mk, Prod.mk, Usa2018P6.usa2018p6_aux.partner, Equiv.Perm, And, Function.Involutive, Ne, Subtype.mk, Usa2018P6.usa2018p6_aux.restrictPerm, Prod.snd, Nat.succ, Equiv.Perm.decomposeFin, Equiv.symm, Fin.succ, Prod.fst, Usa2018P6.usa2018p6_aux.extendPerm
16 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
noncomputable def fpfDecomposeEquiv (n : ℕ) :
    fpfSubtype (n + 2) ≃ Fin (n + 1) × fpfSubtype n where
…
```
Mentions: Usa2018P6.usa2018p6_aux.fpfSubtype
abbrev Usa2018P6.usa2018p6_aux.vtxSplitType The two cases of involutions of Fin (n + 2) with at most one fixed point, according to whether 0 is fixed line 2172 source
Source documentation
The two cases of involutions of Fin (n + 2) with at most one fixed point, according to whether 0 is fixed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Sum, Subtype, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, Ne
11 instances, coercions and auxiliary constants left out.
```
abbrev vtxSplitType (n : ℕ) :=
…
```
def Usa2018P6.usa2018p6_aux.splitZeroEquiv Split involutions of Fin (n + 2) according to whether 0 is a fixed point line 2179 source
Source documentation
Split involutions of Fin (n + 2) according to whether 0 is a fixed point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Usa2018P6.usa2018p6_aux.vtxSubtype, HAdd.hAdd, OfNat.ofNat, Usa2018P6.usa2018p6_aux.vtxSplitType
Proof uses: Equiv.mk, dite, Eq, Fin, Equiv.Perm, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Finset.univ, Sum.inl, Subtype, Ne, Subtype.mk, Not, Sum.inr, Sum.elim
21 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
noncomputable def splitZeroEquiv (n : ℕ) :
    vtxSubtype (n + 2) ≃ vtxSplitType n where
…
```
Mentions: Usa2018P6.usa2018p6_aux.vtxSubtype, Usa2018P6.usa2018p6_aux.vtxSplitType
def Usa2018P6.usa2018p6_aux.vtxZeroEquiv Involutions of Fin (n + 2) with at most one fixed point that fix 0 are in bijection with fixed-point-free involutions of Fin (n + 1) line 2197 source
Source documentation
Involutions of Fin (n + 2) with at most one fixed point that fix 0 are in bijection with fixed-point-free involutions of Fin (n + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Subtype, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, Usa2018P6.usa2018p6_aux.fpfSubtype
Proof uses: Equiv.mk, Subtype.mk, Ne, Prod.snd, Nat.succ, Prod, Equiv.Perm.decomposeFin, Equiv.symm, Prod.mk
29 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def vtxZeroEquiv (n : ℕ) :
    {σ : Equiv.Perm (Fin (n + 2)) //
      (Function.Involutive σ ∧ (Finset.univ.filter fun x => σ x = x).card ≤ 1) ∧ σ 0 = 0} ≃
        fpfSubtype (n + 1) where
…
```
Mentions: Usa2018P6.usa2018p6_aux.fpfSubtype
def Usa2018P6.usa2018p6_aux.vtxSuccEquiv Documented declaration: vtxSuccEquiv line 2218 source
Source documentation
Involutions of Fin (n + 2) with at most one fixed point that move 0 are in bijection with pairs of an element j : Fin (n + 1) and an involution of Fin n with at most one fixed point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Subtype, Equiv.Perm, Fin, HAdd.hAdd, OfNat.ofNat, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, Ne, Prod, Usa2018P6.usa2018p6_aux.vtxSubtype
Proof uses: Equiv.mk, Prod.mk, Usa2018P6.usa2018p6_aux.partner, Subtype.mk, Usa2018P6.usa2018p6_aux.restrictPerm, Prod.snd, Nat.succ, Equiv.Perm.decomposeFin, Equiv.symm, Fin.succ, Prod.fst, Usa2018P6.usa2018p6_aux.extendPerm
30 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
noncomputable def vtxSuccEquiv (n : ℕ) :
    {σ : Equiv.Perm (Fin (n + 2)) //
      (Function.Involutive σ ∧ (Finset.univ.filter fun x => σ x = x).card ≤ 1) ∧ σ 0 ≠ 0} ≃
        Fin (n + 1) × vtxSubtype n where
…
```
Mentions: Usa2018P6.usa2018p6_aux.vtxSubtype
def Usa2018P6.usa2018p6_aux.vtxDecomposeEquiv The full decomposition for involutions with at most one fixed point line 2256 source
Source documentation
The full decomposition for involutions with at most one fixed point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv, Usa2018P6.usa2018p6_aux.vtxSubtype, HAdd.hAdd, OfNat.ofNat, Sum, Usa2018P6.usa2018p6_aux.fpfSubtype, Prod, Fin
Proof uses: Equiv.trans, Usa2018P6.usa2018p6_aux.vtxSplitType, Usa2018P6.usa2018p6_aux.splitZeroEquiv, Equiv.sumCongr, Subtype, Equiv.Perm, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, Ne, Usa2018P6.usa2018p6_aux.vtxZeroEquiv, Usa2018P6.usa2018p6_aux.vtxSuccEquiv
14 instances, coercions and auxiliary constants left out.
```
noncomputable def vtxDecomposeEquiv (n : ℕ) :
    vtxSubtype (n + 2) ≃ fpfSubtype (n + 1) ⊕ Fin (n + 1) × vtxSubtype n :=
…
```
Mentions: Usa2018P6.usa2018p6_aux.vtxSubtype, Usa2018P6.usa2018p6_aux.fpfSubtype
theorem Usa2018P6.usa2018p6_aux.fcard_succ_succ line 2262 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2018P6.usa2018p6_aux.fcard, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: id, Eq.mpr, Fintype.card, Usa2018P6.usa2018p6_aux.fpfSubtype, Prod, Fin, congrArg, Fintype.card_congr, Usa2018P6.usa2018p6_aux.fpfDecomposeEquiv, Fintype.card_prod, Fintype.card_fin, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.vcard_succ_succ line 2266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2018P6.usa2018p6_aux.vcard, HAdd.hAdd, OfNat.ofNat, Usa2018P6.usa2018p6_aux.fcard, HMul.hMul
Proof uses: id, Fintype.card, Usa2018P6.usa2018p6_aux.vtxSubtype, Eq.mpr, Usa2018P6.usa2018p6_aux.fpfSubtype, Sum, Prod, Fin, congrArg, Fintype.card_congr, Usa2018P6.usa2018p6_aux.vtxDecomposeEquiv, Fintype.card_sum, Fintype.card_prod, Fintype.card_fin, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.fcard_zero line 2271 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2018P6.usa2018p6_aux.fcard, OfNat.ofNat
Proof uses: Equiv, Usa2018P6.usa2018p6_aux.fpfSubtype, Equiv.Perm, Fin, Equiv.subtypeUnivEquiv, And, Function.Involutive, Ne, And.intro, Fin.elim0, id, Eq.mpr, Fintype.card, congrArg, Fintype.card_congr, Nat.factorial, Fintype.card_perm, Fintype.card_fin, Nat.factorial_zero, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.fcard_one line 2277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2018P6.usa2018p6_aux.fcard, OfNat.ofNat
Proof uses: id, IsEmpty, Usa2018P6.usa2018p6_aux.fpfSubtype, IsEmpty.mk, And.right, Function.Involutive, Fin, Equiv.Perm, And, Ne, Subtype.property, Fin.eq_zero, Fintype.card_of_isEmpty
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.vcard_zero line 2282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2018P6.usa2018p6_aux.vcard, OfNat.ofNat
Proof uses: Equiv, Usa2018P6.usa2018p6_aux.vtxSubtype, Equiv.Perm, Fin, Equiv.subtypeUnivEquiv, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Finset.univ, And.intro, Fin.elim0, Iff.mpr, Membership.mem, Finset, Finset.card_le_one, id, Eq.mpr, Fintype.card and 7 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.vcard_one line 2289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2018P6.usa2018p6_aux.vcard, OfNat.ofNat
Proof uses: Equiv.Perm, Fin, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Finset.univ, And.intro, Eq.mpr, id, congrArg, Fin.eq_zero, Eq.refl, Iff.mpr, Membership.mem, Finset, Finset.card_le_one, Equiv, Usa2018P6.usa2018p6_aux.vtxSubtype and 7 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.fcard_parity line 2302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, Even, Odd, Usa2018P6.usa2018p6_aux.fcard, Eq, OfNat.ofNat
Proof uses: Nat.twoStepInduction, And.intro, Eq.mpr, id, congrArg, Usa2018P6.usa2018p6_aux.fcard_zero, odd_one, False.elim, Eq.mp, HMod.hMod, False, propext, Nat.odd_iff, Eq.trans, congrFun', Nat.mod_succ, Nat.even_iff, Usa2018P6.usa2018p6_aux.fcard_one, HAdd.hAdd, HMul.hMul and 7 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.usa2018p6_aux.vcard_odd line 2326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Usa2018P6.usa2018p6_aux.vcard
Proof uses: Nat.twoStepInduction, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, Usa2018P6.usa2018p6_aux.vcard_zero, odd_one, Usa2018P6.usa2018p6_aux.vcard_one, HAdd.hAdd, Usa2018P6.usa2018p6_aux.fcard, HMul.hMul, Usa2018P6.usa2018p6_aux.vcard_succ_succ, Even, Or, Nat.even_or_odd, Even.add_one, And.right, Usa2018P6.usa2018p6_aux.fcard_parity, Nat.zero_add and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
theorem Usa2018P6.odd_card_vertex The number of involutions of Fin n with at most one fixed point is odd line 2344 source
Source documentation
The number of involutions of Fin n with at most one fixed point is odd.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Odd, Fintype.card, Subtype, Equiv.Perm, Fin, And, Function.Involutive, LE.le, Finset.card, Finset.filter, Eq, Finset.univ, OfNat.ofNat
Proof uses: Usa2018P6.usa2018p6_aux.vcard_odd
13 instances, coercions and auxiliary constants left out.
```
theorem odd_card_vertex (n : ℕ) :
    Odd (Fintype.card {σ : Equiv.Perm (Fin n) //
      Function.Involutive σ ∧ (Finset.univ.filter fun x => σ x = x).card ≤ 1}) :=
…
```
lemma Usa2018P6.sum_modEq_of_forall Summed Nat.ModEq over a finset line 2352 source
Source documentation
Summed Nat.ModEq over a finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Nat, Membership.mem, Nat.ModEq, OfNat.ofNat, Finset.sum
Proof uses: Finset.induction, EmptyCollection.emptyCollection, Nat.ModEq.rfl, Not, Insert.insert, Eq.mpr, HAdd.hAdd, id, Eq, congrArg, Finset.sum_insert, Nat.ModEq.add, Finset.mem_insert_self, Finset.mem_insert_of_mem
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma sum_modEq_of_forall {ι : Type*} [DecidableEq ι] (s : Finset ι) (f g : ι → ℕ)
    (h : ∀ i ∈ s, f i ≡ g i [MOD 2]) : (∑ i ∈ s, f i) ≡ (∑ i ∈ s, g i) [MOD 2] := by
…
```
Mentions: f, h
problem Usa2018P6.usa2018_p6 USAMO 2018, Problem 6: the number of permutations of (1, …, n) whose ratios xₖ/k are all distinct is odd for every n ≥ 1 line 2363 source
Source documentation
USAMO 2018, Problem 6: the number of permutations of (1, …, n) whose ratios xₖ/k are all distinct is odd for every n ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Odd, Fintype.card, Subtype, Equiv.Perm, Fin, Usa2018P6.Valid
Proof uses: Nat.ModEq, And, Function.Involutive, Subtype.mk, Inv.inv, Usa2018P6.valid_inv, Subtype.property, Subtype.ext, id, Eq, inv_inv, Usa2018P6.card_modEq_of_involutive, Fintype.card_congr, Equiv.mk, And.intro, congrArg, HMul.hMul, Iff.mpr, mul_eq_one_iff_eq_inv, Eq.symm and 70 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
problem usa2018_p6 (n : ℕ) (_hn : 1 ≤ n) :
    Odd (Fintype.card {σ : Equiv.Perm (Fin n) // Valid σ}) := by
…
```
Mentions: Usa2018P6.Valid