From 10edba2c0365a6858a74da22042c98f9d5fa1acc Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 26 Oct 2025 01:19:45 +0200 Subject: simplify FPerm computations --- Nominal/Permutations.lean | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'Nominal/Permutations.lean') diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index 62d7470..1726ed7 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -138,13 +138,20 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by apply ext simp [swap] -/-- If c is not equal to a or b, then (a b) leaves c unchanged. -/ -lemma swap_neq {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by +/-- Lifting of Equiv.swap_apply_of_ne_of_ne to finite permutations. -/ +lemma swap_apply_of_ne_of_ne {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by intro ha hb - apply Equiv.Perm.supp_notin - simp only [swap, Equiv.Perm.supp_swap, ne_eq, ite_not, Set.mem_ite_empty_left, Set.mem_insert_iff, Set.mem_singleton_iff, not_and, not_or] - intro _ - exact ⟨ha, hb⟩ + simp [swap, Equiv.swap_apply_of_ne_of_ne, ha, hb] + +/-- Lifting of Equiv.swap_apply_left to finite permutations. -/ +@[simp] +lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by + simp [swap] + +/-- Lifting of Equiv.swap_apply_right to finite permutations. -/ +@[simp] +lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by + simp [swap] end FPerm -- cgit v1.3.1