diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 89021a0..430aa8c 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -62,7 +62,8 @@ lemma support_inter {x : X} {S T : Set 𝔸} : HasSupport 𝔸 x S → S.Finite -- First we obtain an injection m : S \ T → (π'.supp ∪ S ∪ T)ᶜ. have h_cod_inf : ((π'.supp ∪ S ∪ T)ᶜ).Infinite := by apply Set.Finite.infinite_compl - simp; exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩ + simp only [Set.finite_union] + exact ⟨⟨h_π_fin, h_S_finite⟩, h_T_finite⟩ have h_dom_fin : (S \ T).Finite := Set.Finite.diff h_S_finite @@ -308,7 +309,7 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ PermSet.fix' 𝔸 x := by intro ha hb suffices ⸨a, b⸩ • x = (1 : FPerm 𝔸) • x by - simp only [one_smul, PermSet.fix', Set.mem_setOf_eq] at *; assumption + simp [one_smul, PermSet.fix'] at *; assumption apply PermSet.support_permutations_eq · exact supp_is_support 𝔸 · intro c hc @@ -316,13 +317,13 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by - simp [NominalSet.ForFresh]; intro h + simp only [ForFresh]; intro h exact h.nonempty /-- Extensionality lemma for the freshness quantifier. -/ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) = (И a, Q a) := by intro h - simp [NominalSet.ForFresh] + simp only [ForFresh, eq_iff_iff] suffices {a | P a} = {a | Q a} by rw [this] exact Set.ext h |