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/Instances/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Nominal/Instances/Basic.lean') 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₂ -- cgit v1.3.1