diff options
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 368d266..50cf7c2 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -38,7 +38,7 @@ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𔸠S ↔ ∀ (x : X) (Ï Â· intro hx; exact h x Ï€ hx · intro hx apply (h (Ï€ • x) Ï€â»Â¹) at hx - simp at hx + simp only [inv_smul_smul] at hx exact hx · intro h x Ï€ hx exact (h x Ï€).mp hx @@ -50,7 +50,7 @@ lemma equivariant_relation_iff {R : Rel X Y} : EquivariantRelation 𔸠R ↔ ∠· intro hxy; exact h x y Ï€ hxy · intro hxy apply (h (Ï€ • x) (Ï€ • y) Ï€â»Â¹) at hxy - simp at hxy + simp only [inv_smul_smul] at hxy exact hxy · intro h x y Ï€ hxy exact (h x y Ï€).mp hxy @@ -201,7 +201,7 @@ private lemma for_fresh_iffâ‚ : EquivariantRelation 𔸠R → (И a, R a x) ↠intro hequi h have hinf : ({a | R a x} \ NominalSet.supp 𔸠x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite ð”¸) obtain ⟨a, ha⟩ := hinf.nonempty - simp at ha + simp only [Set.mem_diff, Set.mem_setOf_eq] at ha use a; exact ha.symm private lemma for_fresh_iffâ‚‚ : EquivariantRelation 𔸠R → (∃ a, a # x ∧ R a x) → (∀ a, a # x → R a x) := by @@ -220,7 +220,7 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𔸠R → (∀ a, a # x ↠intro a ha rw [Set.mem_compl_iff] at ha exact h a ha - simp [NominalSet.ForFresh] + simp only [NominalSet.ForFresh] apply Set.infinite_of_finite_compl apply Set.Finite.subset (NominalSet.supp_finite ð”¸) hsub |