simplify FPerm computations

4 files changed, 22 insertions, 21 deletions

diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean
index 508167e..660c2ab 100644
--- a/Nominal/Instances/Abstraction.lean
+++ b/Nominal/Instances/Abstraction.lean
@@ -147,19 +147,10 @@ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.at
         simp at hcy
         have h_atom : (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • c # (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • x.body :=
           NominalSet.fresh_equivariant 𝔸 _ _ _ hcx.right
-        -- TODO: Refactor into lemma
         have h_swap : ⸨c, x.atom⸩ * ⸨c, y.atom⸩ = ⸨x.atom, y.atom⸩ * ⸨c, x.atom⸩ := by
           ext a
-          simp [FPerm.swap]
-          by_cases h₁ : (a = c) <;> by_cases h₂ : (a = x.atom) <;> by_cases h₃ : (a = y.atom)
-          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
-          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
-          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
-          · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
-          · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left]
-          · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left]
-          · simp [h₃, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)]
-          · simp [Equiv.swap_apply_of_ne_of_ne h₁ h₃, Equiv.swap_apply_of_ne_of_ne h₁ h₂, Equiv.swap_apply_of_ne_of_ne h₂ h₃]
+          by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom
+          all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h_eq]
         rw [mul_smul, PermSet.atom_swap, PermSet.atom_swap, Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq] at h_atom
         rw [mul_smul, hc, ← mul_smul, FPerm.swap_mul_self, one_smul] at h_atom
         constructor
@@ -171,10 +162,13 @@ lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.at
             _      = ⸨x.atom, y.atom⸩ • y.body               := by rw [NominalSet.fresh_swap_fix 𝔸 hcy.right h_atom]
     · rw [alpha_eq_iff_all]
       intro h c ⟨hcx, hcy⟩
+      simp at hcx
       simp at hcy
       simp only [h_eq, false_and, ne_eq, not_false_eq_true, true_and, false_or] at h
-      -- TODO: Use new lemma from before
-      have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := sorry
+      have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := by
+        ext a
+        by_cases a = c <;> by_cases a = x.atom <;> by_cases a = y.atom
+        all_goals simp_all [FPerm.swap_apply_of_ne_of_ne, hcy.left, hcx.left, Ne.symm hcy.left, Ne.symm hcx.left, Ne.symm h_eq]
       rw [h.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.left]
 
 private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 2786c86..2bb389d 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -41,7 +41,7 @@ instance : NominalSet 𝔸 𝔸 where
     simp only [Finset.singleton_union, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc
     have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by
       intro d hd
-      apply FPerm.swap_neq (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right)
+      apply FPerm.swap_apply_of_ne_of_ne (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right)
     have h₁ : ⸨a, c⸩ • a = c := by rw [PermSet.atom_swap, Equiv.swap_apply_left]
     have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption
     rw [h₁] at h₂
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
 
diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 430aa8c..d80503f 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -313,7 +313,7 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P
   apply PermSet.support_permutations_eq
   · exact supp_is_support 𝔸
   · intro c hc
-    apply FPerm.swap_neq (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb)
+    apply FPerm.swap_apply_of_ne_of_ne (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb)
 
 /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/
 lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by