diff options
Diffstat (limited to 'Nominal/Permutations.lean')
| -rw-r--r-- | Nominal/Permutations.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index a583b4c..b8d510e 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -31,7 +31,7 @@ theorem mem_supp (π : Equiv.Perm X) (x : X) : x ∈ π.supp ↔ π x ≠ x := b /-- If an element does not occur in the support, the permutation doesn't move it. -/ lemma supp_notin {π : Equiv.Perm X} {x : X} : x ∉ π.supp → π x = x := by - rw [show (π x = x) ↔ ¬(π x ≠ x) by simp] + rw [show (π x = x) ↔ ¬(π x ≠ x) by simp only [ne_eq, not_not]] simp [← (mem_supp π x).not] /-- The support of the identity function is the empty set. -/ @@ -46,7 +46,7 @@ lemma supp_inv (π : Equiv.Perm X) : π⁻¹.supp = π.supp := by /-- The support of two concatenated permutations is a subset of the individual supports as a union. -/ lemma supp_mul_subset (π τ : Equiv.Perm X) : (π * τ).supp ⊆ π.supp ∪ τ.supp := by - simp [supp] + simp only [supp, coe_mul, Function.comp_apply, ne_eq] apply set_support_mul_subset end Equiv.Perm |