diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 18:20:43 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 18:20:43 +0200 |
| commit | 6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521 (patch) | |
| tree | c56ca4d707e88d49c0f52e99d5e1c07edb58e3fe /Nominal/Permutations.lean | |
| parent | ac2363701c3d2a03116af449ca7bc4f918fbfda7 (diff) | |
use simp only everywhere except for last goal
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 |