From 6df3f662f0f23e837b70ef1f4a8b8dde4a7aa521 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 24 Oct 2025 18:20:43 +0200 Subject: use simp only everywhere except for last goal --- Nominal/Permutations.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Nominal/Permutations.lean') 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 -- cgit v1.3.1