diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:19:45 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:20:20 +0200 |
| commit | 10edba2c0365a6858a74da22042c98f9d5fa1acc (patch) | |
| tree | e8d1b29734b02cf654d91f6b33921915e108b296 /Nominal/Instances/Basic.lean | |
| parent | c3700706466cb8fb9ed287ea066b656caacdc9c7 (diff) | |
simplify FPerm computations
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 2 |
1 files changed, 1 insertions, 1 deletions
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₂ |