From 2489e2d5da786d6da0bda30f092c9622cc7d3f81 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 24 Oct 2025 01:31:41 +0200
Subject: fill in some proofs

---
 Nominal/Permutations.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'Nominal/Permutations.lean')

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 4a3e88f..1bcb00f 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -116,6 +116,11 @@ end Equiv.Perm
 
 namespace FPerm
 
+/-- Extensionality lemma for finite permutations. -/
+lemma ext {X : Type} {π₁ π₂ : FPerm X} : π₁.val = π₂.val → π₁ = π₂ := by
+  intro h; ext; rw [h]
+
+/-- Transpositions are finite permutations. -/
 def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
   apply Set.Finite.subset
   · apply ({x, y} : Finset X).finite_toSet
@@ -123,6 +128,11 @@ def swap (x y : X) : FPerm X := ⟨Equiv.swap x y, by
 
 notation "⸨" a "," b "⸩" => FPerm.swap a b
 
+/-- Lifting of Equiv.mul_swap_eq_swap_mul to finite permutations. -/
+lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, π b⸩ * π := by
+  apply ext
+  apply Equiv.mul_swap_eq_swap_mul
+
 end FPerm
 
 example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩
-- 
cgit v1.3.1