Support refactor fixes

Signed-off-by: zeramorphic <[email protected]>

ConNF/FOA/Basic/Constrains.lean

@@ -405,9 +405,9 @@ theorem small_constrains {β : Λ} (c : SupportCondition β) : Small {d | d ≺
     · obtain ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, B, t, rfl, rfl⟩ := h
       refine lt_of_le_of_lt ?_ (designatedSupport t).small
       suffices
-        #{a : SupportCondition β |
-            ∃ c : designatedSupport t, a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤
-          #(designatedSupport t) by
+        #{a : SupportCondition β | ∃ c : (designatedSupport t : Set (SupportCondition δ)),
+            a = ⟨(B.cons hδ).comp c.val.path, c.val.value⟩} ≤
+          #(designatedSupport t : Set (SupportCondition δ)) by
         refine le_trans (Cardinal.mk_subtype_le_of_subset ?_) this
         rintro x ⟨_, _, _, _, _, _, _, _, _, _, _, c, hc, rfl, h⟩
         rw [SupportCondition.mk.injEq] at h

ConNF/FOA/Basic/Reduction.lean

@@ -184,29 +184,8 @@ theorem reduction_supports (S : Set (SupportCondition β)) (c : SupportCondition
 theorem reduction_designatedSupport_supports [TangleData β] (t : Tangle β) :
     Supports (Allowable β) (reduction (designatedSupport t : Set (SupportCondition β))) t := by
   intro ρ h
-  refine (designatedSupport t).supports ρ ?_
+  refine designatedSupport_supports t ρ ?_
   intros c hc'
   exact reduction_supports (designatedSupport t) c hc' (Allowable.toStructPerm ρ) h
 
-/-- A support for a tangle containing only reduced support conditions. -/
-noncomputable def reducedSupport [TangleData β] (t : Tangle β) : Support β (Allowable β) t
-    where
-  carrier := reduction (designatedSupport t : Set (SupportCondition β))
-  small := reduction_small (designatedSupport t).small
-  supports := reduction_designatedSupport_supports t
-
-theorem mem_reducedSupport_iff [TangleData β] (t : Tangle β) (c : SupportCondition β) :
-    c ∈ reducedSupport t ↔ c ∈ reduction (designatedSupport t : Set (SupportCondition β)) :=
-  Iff.rfl
-
-theorem lt_of_mem_reducedSupport
-    {β γ δ ε : Λ} [LeLevel β] [LeLevel γ] [LtLevel δ] [LtLevel ε]
-    (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < γ) (hδε : (δ : TypeIndex) ≠ ε)
-    (B : Path (β : TypeIndex) γ) (t : Tangle δ)
-    (c : SupportCondition δ) (h : c ∈ reducedSupport t) :
-    (⟨(B.cons hδ).comp c.path, c.value⟩ : SupportCondition β) <
-      ⟨(B.cons hε).cons (bot_lt_coe _), inr (fuzz hδε t).toNearLitter⟩ := by
-  obtain ⟨⟨d, hd, hcd⟩, _⟩ := h
-  exact Relation.TransGen.tail' (le_comp hcd _) (Constrains.fuzz hδ hε hδε B t d hd)
-
 end ConNF

ConNF/FOA/Properties/Injective.lean

@@ -218,7 +218,7 @@ theorem Biexact.smul_eq_smul {β : Λ} [LeLevel β] {π π' : Allowable β} {c :
     refine h₁.trans (h₂.trans ?_).symm
     refine' congr_arg _ _
     rw [← inv_smul_eq_iff, smul_smul]
-    refine' (designatedSupport t).supports _ _
+    refine' designatedSupport_supports t _ _
     intro c hc
     rw [mul_smul, inv_smul_eq_iff]
     simp only [Allowable.toStructPerm_smul, Allowable.toStructPerm_comp, Tree.comp_comp]
@@ -423,7 +423,7 @@ theorem supports {β : Λ} [LeLevel β] {π π' : Allowable β} {t : Tangle β}
       Allowable.toStructPerm π' A • N) :
     π • t = π' • t := by
   rw [← inv_smul_eq_iff, smul_smul]
-  refine' (designatedSupport t).supports _ _
+  refine' designatedSupport_supports t _ _
   intro c hc
   rw [mul_smul, inv_smul_eq_iff]
   simp only [Allowable.smul_supportCondition_eq_smul_iff]
@@ -802,7 +802,7 @@ theorem ihAction_smul_tangle' (hπf : π.Free) (c d : SupportCondition β) (A :
         (ihsAction_comp_mapFlexible hπf _ _ _) • hL₂.t := by
   obtain ⟨⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩, t, rfl⟩ := hL₂
   rw [← inv_smul_eq_iff, smul_smul]
-  refine' (designatedSupport t).supports _ _
+  refine' designatedSupport_supports t _ _
   intro e he
   rw [mul_smul, inv_smul_eq_iff]
   simp only [ne_eq, Allowable.smul_supportCondition_eq_smul_iff]

ConNF/Fuzz/Hypotheses.lean

@@ -145,14 +145,11 @@ instance Bot.tangleData : TangleData ⊥
   Allowable := NearLitterPerm
   allowableToStructPerm := Tree.toBotIso.toMonoidHom
   allowableAction := inferInstance
-  designatedSupport a := ⟨1, _⟩
-    -- { carrier := {⟨Quiver.Path.nil, Sum.inl a⟩}
-    --   supports := fun π => by
-    --     intro h
-    --     simp only [mem_singleton_iff, NearLitterPerm.smul_supportCondition_eq_iff, forall_eq,
-    --       Sum.smul_inl, Sum.inl.injEq] at h
-    --     exact h
-    --   small := small_singleton _ }
+  designatedSupport a := ⟨1, fun _ _ => ⟨Quiver.Path.nil, Sum.inl a⟩⟩
+  designatedSupport_supports a π h := by
+    simp only [Support.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
+      NearLitterPerm.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inl, Sum.inl.injEq] at h
+    exact h
 
 /-- A position function for atoms, which is chosen arbitrarily. -/
 noncomputable instance instPositionAtom : Position Atom μ :=

ConNF/NewTangle/NewTangle.lean

@@ -400,7 +400,8 @@ end NewAllowable
 This is `τ_α` in the blueprint.
 Unlike the type `tangle`, this is not an opaque definition, and we can inspect and unfold it. -/
 def NewTangle :=
-  { t : Semitangle // Supported α NewAllowable t }
+  { t : Semitangle //
+    ∃ S : Support α, MulAction.Supports NewAllowable (S : Set (SupportCondition α)) t }
 
 variable {c d : Code} {S : Set (SupportCondition α)}
 
@@ -419,9 +420,11 @@ theorem Code.Equiv.supports_iff (hcd : c ≡ d) :
 
 /-- If two codes are equivalent, one is supported if and only if the other is. -/
 theorem Code.Equiv.supported_iff (hcd : c ≡ d) :
-    Supported α NewAllowable c ↔ Supported α NewAllowable d :=
-  ⟨fun ⟨⟨s, hs, h⟩⟩ => ⟨⟨s, hs, hcd.supports h⟩⟩,
-    fun ⟨⟨s, hs, h⟩⟩ => ⟨⟨s, hs, hcd.symm.supports h⟩⟩⟩
+    (∃ S : Support α, MulAction.Supports NewAllowable (S : Set (SupportCondition α)) c) ↔
+    ∃ S : Support α, MulAction.Supports NewAllowable (S : Set (SupportCondition α)) d := by
+  constructor <;> rintro ⟨S, hS⟩
+  · exact ⟨S, hcd.supports hS⟩
+  · exact ⟨S, hcd.symm.supports hS⟩
 
 @[simp]
 theorem smul_intro {β : TypeIndex} [inst : LtLevel β]  (ρ : NewAllowable) (s : Set (Tangle β)) (hs) :
@@ -457,17 +460,19 @@ theorem NewAllowable.smul_supportCondition_eq_smul_iff
 This is called a *typed near litter*. -/
 def newTypedNearLitter (N : NearLitter) : NewTangle :=
   ⟨intro (show Set (Tangle ⊥) from N.2.1) <| Code.isEven_bot _,
-    ⟨⟨{⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩}, small_singleton _, fun ρ h => by
-        simp only [smul_intro]
-        congr 1
-        simp only [mem_singleton_iff, NewAllowable.smul_supportCondition_eq_iff, forall_eq,
-          Sum.smul_inr, Sum.inr.injEq] at h
-        apply_fun SetLike.coe at h
-        refine Eq.trans ?_ h
-        rw [NearLitterPerm.smul_nearLitter_coe]
-        change _ '' _ = _ '' _
-        simp_rw [SemiallowablePerm.coe_apply_bot]
-        rfl⟩⟩⟩
+    ⟨1, fun _ _ => ⟨Quiver.Hom.toPath (bot_lt_coe _), Sum.inr N⟩⟩,
+    by
+      intro ρ h
+      simp only [smul_intro]
+      congr 1
+      simp only [Support.mem_carrier_iff, κ_lt_one_iff, exists_prop, exists_eq_left,
+        NewAllowable.smul_supportCondition_eq_iff, forall_eq, Sum.smul_inr, Sum.inr.injEq] at h
+      apply_fun SetLike.coe at h
+      refine Eq.trans ?_ h
+      rw [NearLitterPerm.smul_nearLitter_coe]
+      change _ '' _ = _ '' _
+      simp_rw [SemiallowablePerm.coe_apply_bot]
+      rfl⟩
 
 namespace NewTangle
 
@@ -486,17 +491,18 @@ namespace NewAllowable
 instance hasSmulNewTangle : SMul NewAllowable NewTangle :=
   ⟨fun ρ t =>
     ⟨ρ • (t : Semitangle),
-      t.2.map fun (s : Support α NewAllowable (t : Semitangle)) =>
-        { carrier := ρ • (s : Set (SupportCondition α))
-          small := s.small.image
-          supports := by
-            intro ρ' h
-            have := s.supports (ρ⁻¹ * ρ' * ρ) ?_
-            · conv_rhs =>
-                rw [← this, ← mul_smul, ← mul_assoc, ← mul_assoc, mul_inv_self, one_mul, mul_smul]
-            · intro a ha
-              rw [mul_smul, mul_smul, inv_smul_eq_iff]
-              exact h (smul_mem_smul_set ha) }⟩⟩
+      by
+        obtain ⟨S, hS⟩ := t.2
+        refine ⟨ρ • S, ?_⟩
+        intro ρ' h
+        have := hS (ρ⁻¹ * ρ' * ρ) ?_
+        · conv_rhs =>
+            rw [← this, ← mul_smul, ← mul_assoc, ← mul_assoc, mul_inv_self, one_mul, mul_smul]
+        · intro a ha
+          rw [mul_smul, mul_smul, inv_smul_eq_iff]
+          refine h ?_
+          simp only [Support.mem_carrier_iff, smul_carrier, smul_mem_smul_set_iff] at ha ⊢
+          exact ha⟩⟩
 
 @[simp, norm_cast]
 theorem coe_smul_newTangle (ρ : NewAllowable) (t : NewTangle) :

ConNF/Structural/Support.lean

@@ -15,7 +15,7 @@ In this file, we define support conditions and supports.
 
 open Cardinal Equiv
 
-open scoped Cardinal
+open scoped Cardinal Pointwise
 
 universe u
 
@@ -126,12 +126,28 @@ def Support.carrier (S : Support α) : Set (SupportCondition α) :=
 instance : CoeTC (Support α) (Set (SupportCondition α)) where
   coe S := S.carrier
 
+instance : Membership (SupportCondition α) (Support α) where
+  mem c S := c ∈ S.carrier
+
+@[simp]
+theorem Support.mem_carrier_iff (c : SupportCondition α) (S : Support α) :
+    c ∈ S.carrier ↔ ∃ i, ∃ (h : i < S.max), c = S.f i h :=
+  Iff.rfl
+
+@[simp]
+theorem Support.mem_iff (c : SupportCondition α) (S : Support α) :
+    c ∈ S ↔ ∃ i, ∃ (h : i < S.max), c = S.f i h :=
+  Iff.rfl
+
 theorem Support.carrier_small (S : Support α) : Small S.carrier := by
   refine lt_of_le_of_lt (b := #(Set.Iio S.max)) ?_ (card_typein_lt (· < ·) S.max Params.κ_ord.symm)
   refine mk_le_of_surjective (f := fun x => ⟨S.f x x.prop, x, x.prop, rfl⟩) ?_
   rintro ⟨_, i, h, rfl⟩
   exact ⟨⟨i, h⟩, rfl⟩
 
+theorem Support.small (S : Support α) : Small (S : Set (SupportCondition α)) :=
+  S.carrier_small
+
 def supportEquiv : Support α ≃ Σ max : κ, Set.Iio max → SupportCondition α where
   toFun S := ⟨S.max, fun x => S.f x x.prop⟩
   invFun S := ⟨S.1, fun i h => S.2 ⟨i, h⟩⟩
@@ -225,4 +241,49 @@ theorem mk_support_le : #(Support α) ≤ #μ := by
   · simp only [sum_const, lift_id, mul_mk_eq_max, ge_iff_le, max_le_iff, le_refl, and_true]
     exact Params.κ_lt_μ.le
 
+instance {G : Type _} [SMul G (SupportCondition α)] : SMul G (Support α) where
+  smul g S := ⟨S.max, fun i hi => g • S.f i hi⟩
+
+@[simp]
+theorem smul_max {G : Type _} [SMul G (SupportCondition α)] (g : G) (S : Support α) :
+    (g • S).max = S.max :=
+  rfl
+
+@[simp]
+theorem smul_f {G : Type _} [SMul G (SupportCondition α)]
+    (g : G) (S : Support α) (i : κ) (hi : i < S.max) :
+    (g • S).f i hi = g • S.f i hi :=
+  rfl
+
+@[simp]
+theorem smul_carrier {G : Type _} [SMul G (SupportCondition α)] (g : G) (S : Support α) :
+    (g • S).carrier = g • S.carrier := by
+  ext x : 1
+  constructor
+  · rintro ⟨i, hi, h⟩
+    exact ⟨_, ⟨i, hi, rfl⟩, h.symm⟩
+  · rintro ⟨_, ⟨i, hi, rfl⟩, h⟩
+    exact ⟨i, hi, h.symm⟩
+
+@[simp]
+theorem smul_coe {G : Type _} [SMul G (SupportCondition α)] (g : G) (S : Support α) :
+    (g • S : Support α) = g • (S : Set (SupportCondition α)) :=
+  smul_carrier g S
+
+instance {G : Type _} [Monoid G] [MulAction G (SupportCondition α)] : MulAction G (Support α) where
+  one_smul := by
+    rintro ⟨i, f⟩
+    ext
+    · rfl
+    · refine heq_of_eq (funext₂ ?_)
+      intro j hj
+      simp only [smul_f, one_smul]
+  mul_smul g h := by
+    rintro ⟨i, f⟩
+    ext
+    · rfl
+    · refine heq_of_eq (funext₂ ?_)
+      intro j hj
+      simp only [smul_f, mul_smul]
+
 end ConNF