1 files changed, 46 insertions, 38 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 19b8566..82fd683 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -58,7 +58,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅.
 -/
 section Discrete
 
-def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
+def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where
   smul π x := x
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
@@ -69,21 +69,21 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
     · intro π hπ; simp [PermSet.fix']; rfl
     · exact Set.finite_empty
 
-@[simp] lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
+@[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
   rw [← Set.subset_empty_iff]
   apply Set.sInter_subset_of_mem
   constructor
-  · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete]
+  · intro π hπ; simp [PermSet.fix', is_discrete]
   · exact Set.finite_empty
 
-@[simp] lemma NominalSet.fresh_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {a : 𝔸} {x : X} : a # x := by
+@[simp] lemma NominalSet.Discrete.fresh {X : Type} [NominalSet.Discrete 𝔸 X] {a : 𝔸} {x : X} : a # x := by
   simp [IsFresh]
 
 /-- We consider Unit a discrete nominal set. -/
-instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
+instance : NominalSet.Discrete 𝔸 Unit := NominalSet.discrete 𝔸 Unit
 
 /-- We consider Bool a discrete nominal set. -/
-instance : DiscreteNominalSet 𝔸 Bool := NominalSet.discrete 𝔸 Bool
+instance : NominalSet.Discrete 𝔸 Bool := NominalSet.discrete 𝔸 Bool
 
 end Discrete
 
@@ -94,25 +94,27 @@ Pairs of two nominal sets also form a nominal set, where supp (x, y) = supp x �
 -/
 section Products
 
+namespace Prod
+
 instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X × Y) where
 
 variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
-private lemma NominalSet.supp_product' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (supp 𝔸 x ∪ supp 𝔸 y) := by
+private lemma supp' {x : X} {y : Y} : PermSet.HasSupport 𝔸 (x, y) (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y) := by
   intro π hπ
   obtain ⟨hπ₁, hπ₂⟩ := PermSet.fix_union 𝔸 hπ
-  exact Prod.mk_inj.mpr ⟨supp_is_support 𝔸 hπ₁, supp_is_support 𝔸 hπ₂⟩
+  exact Prod.mk_inj.mpr ⟨NominalSet.supp_is_support 𝔸 hπ₁, NominalSet.supp_is_support 𝔸 hπ₂⟩
 
 instance : NominalSet 𝔸 (X × Y) where
   fin_supp := by
     intro ⟨x, y⟩; use NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y
-    exact ⟨NominalSet.supp_product' 𝔸, Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)⟩
+    exact ⟨supp' 𝔸, Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)⟩
 
-@[simp] lemma NominalSet.supp_product {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 x ∪ supp 𝔸 y := by
+@[simp] lemma supp {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y := by
   ext b; constructor
-  · apply support_subset_supp
-    · exact supp_product' 𝔸
-    · exact Set.Finite.union (supp_finite 𝔸) (supp_finite 𝔸)
+  · apply NominalSet.support_subset_supp
+    · exact supp' 𝔸
+    · exact Set.Finite.union (NominalSet.supp_finite 𝔸) (NominalSet.supp_finite 𝔸)
   · intro hb; cases hb with
     | inl hx =>
         intro S hS
@@ -127,18 +129,20 @@ instance : NominalSet 𝔸 (X × Y) where
         suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right
         exact (hS.out.left hπ).out
 
-@[simp] lemma NominalSet.fresh_product {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by
-  simp [IsFresh]
+@[simp] lemma fresh {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by
+  simp [NominalSet.IsFresh]
 
-lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 (y, x) := by
+lemma supp_comm {x : X} {y : Y} : NominalSet.supp 𝔸 (x, y) = NominalSet.supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
-lemma Prod.fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by
+lemma fst_equivariant : Equivariant 𝔸 (Prod.fst : X × Y → X) := by
   simp [Equivariant]
 
-lemma Prod.snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
+lemma snd_equivariant : Equivariant 𝔸 (Prod.snd : X × Y → Y) := by
   simp [Equivariant]
 
+end Prod
+
 end Products
 
 /-!
@@ -148,59 +152,63 @@ Sums of two nominal sets also form a nominal set, where supp (inl x) = supp x an
 -/
 section Coproducts
 
+namespace Sum
+
 instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X ⊕ Y) where
 
 variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
-private lemma NominalSet.supp_coproduct₁' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (supp 𝔸 x) := by
+private lemma supp_inl' {x : X} : PermSet.HasSupport 𝔸 (.inl x : X ⊕ Y) (NominalSet.supp 𝔸 x) := by
   intro π hπ
   simp [PermSet.fix']
-  exact supp_is_support 𝔸 hπ
+  exact NominalSet.supp_is_support 𝔸 hπ
 
-private lemma NominalSet.supp_coproduct₂' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (supp 𝔸 y) := by
+private lemma supp_inr' {y : Y} : PermSet.HasSupport 𝔸 (.inr y : X ⊕ Y) (NominalSet.supp 𝔸 y) := by
   intro π hπ
   simp [PermSet.fix']
-  exact supp_is_support 𝔸 hπ
+  exact NominalSet.supp_is_support 𝔸 hπ
 
 instance : NominalSet 𝔸 (X ⊕ Y) where
   fin_supp := by
     intro xy
     cases xy with
-    | inl x => use NominalSet.supp 𝔸 x; exact ⟨NominalSet.supp_coproduct₁' 𝔸, NominalSet.supp_finite 𝔸⟩
-    | inr y => use NominalSet.supp 𝔸 y; exact ⟨NominalSet.supp_coproduct₂' 𝔸, NominalSet.supp_finite 𝔸⟩
+    | inl x => use NominalSet.supp 𝔸 x; exact ⟨supp_inl' 𝔸, NominalSet.supp_finite 𝔸⟩
+    | inr y => use NominalSet.supp 𝔸 y; exact ⟨supp_inr' 𝔸, NominalSet.supp_finite 𝔸⟩
 
-@[simp] lemma NominalSet.supp_coproduct₁ {x : X} : supp 𝔸 (.inl x : X ⊕ Y) = supp 𝔸 x := by
+@[simp] lemma supp_inl {x : X} : NominalSet.supp 𝔸 (.inl x : X ⊕ Y) = NominalSet.supp 𝔸 x := by
   ext b; constructor
-  · apply support_subset_supp
-    · exact supp_coproduct₁' 𝔸
-    · exact supp_finite 𝔸
+  · apply NominalSet.support_subset_supp
+    · exact supp_inl' 𝔸
+    · exact NominalSet.supp_finite 𝔸
   · intro hb S hS
     suffices PermSet.HasSupport 𝔸 x S by apply hb; exact ⟨this, hS.out.right⟩
     intro π hπ
     suffices π ∈ PermSet.fix' 𝔸 (.inl x : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
     exact (hS.out.left hπ).out
 
-@[simp] lemma NominalSet.supp_coproduct₂ {y : Y} : supp 𝔸 (.inr y : X ⊕ Y) = supp 𝔸 y := by
+@[simp] lemma supp_inr {y : Y} : NominalSet.supp 𝔸 (.inr y : X ⊕ Y) = NominalSet.supp 𝔸 y := by
   ext b; constructor
-  · apply support_subset_supp
-    · exact supp_coproduct₂' 𝔸
-    · exact supp_finite 𝔸
+  · apply NominalSet.support_subset_supp
+    · exact supp_inr' 𝔸
+    · exact NominalSet.supp_finite 𝔸
   · intro hb S hS
     suffices PermSet.HasSupport 𝔸 y S by apply hb; exact ⟨this, hS.out.right⟩
     intro π hπ
     suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
     exact (hS.out.left hπ).out
 
-@[simp] lemma NominalSet.fresh_coproduct₁ {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by
-  simp [IsFresh]
+@[simp] lemma fresh_inl {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by
+  simp [NominalSet.IsFresh]
 
-@[simp] lemma NominalSet.fresh_coproduct₂ {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
-  simp [IsFresh]
+@[simp] lemma fresh_inr {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
+  simp [NominalSet.IsFresh]
 
-lemma Sum.inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
+lemma inl_equivariant : Equivariant 𝔸 (Sum.inl : X → X ⊕ Y) := by
   simp [Equivariant]
 
-lemma Sum.inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
+lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
   simp [Equivariant]
 
+end Sum
+
 end Coproducts