Migrate to maybedetangled construction

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

ConNF/Counting/Conclusions.lean

@@ -65,11 +65,32 @@ theorem mk_tangle_le (β : Λ) [LeLevel β] : #(Tangle β) ≤ #(TSet β) * #(Su
   simp only [Prod.mk.injEq] at h
   exact Tangle.ext t₁ t₂ h.1 h.2
 
+theorem exists_tangle [i : CountingAssumptions] {β : TypeIndex} [iβ : LeLevel β] (t : TSet β) :
+    ∃ u : Tangle β, u.set = t := by
+  revert i iβ
+  change (_ : _) → _
+  refine WithBot.recBotCoe ?_ ?_ β
+  · intro _ _ t
+    exact ⟨t, rfl⟩
+  · intro β _ _ t
+    obtain ⟨S, hS⟩ := t.has_support
+    exact ⟨⟨t, S, hS⟩, rfl⟩
+
+protected noncomputable def Tangle.typedAtom (β : Λ) [LeLevel β] (a : Atom) : Tangle β :=
+  (exists_tangle (typedAtom a)).choose
+
+protected noncomputable def Tangle.typedAtom_injective (β : Λ) [LeLevel β] :
+    Function.Injective (Tangle.typedAtom β) := by
+  intro a₁ a₂ h
+  refine (typedAtom (α := β)).injective ?_
+  rw [← (exists_tangle (typedAtom a₁)).choose_spec, ← (exists_tangle (typedAtom a₂)).choose_spec]
+  exact congr_arg Tangle.set h
+
 theorem mk_tangle (β : Λ) [LeLevel β] (hzero : #(CodingFunction 0) < #μ) : #(Tangle β) = #μ := by
   refine le_antisymm ?_ ?_
   · refine le_trans (mk_tangle_le β) ?_
     exact mul_le_of_le (mk_tSet_le β hzero) mk_support.le Params.μ_isStrongLimit.isLimit.aleph0_le
-  · have := mk_le_of_injective (typedAtom (α := β)).injective
+  · have := mk_le_of_injective (Tangle.typedAtom_injective β)
     simp only [mk_atom] at this
     exact this
 

ConNF/FOA/Basic/Constrains.lean

@@ -77,16 +77,12 @@ theorem Constrains.hasPosition_lt {c d : Address β} (h : c ≺ d) :
     have := pos_lt_pos_fuzz_nearLitter hδε t (ConNF.fuzz hδε t).toNearLitter rfl
     obtain ⟨B, a | N⟩ := c
     · simp only [Address.pos_atom, Address.pos_nearLitter]
-      by_cases h : t = typedAtom a
-      · subst h
-        rw [pos_typedAtom] at this
-        exact this
+      by_cases h : t.set = typedAtom a
+      · exact (pos_typedAtom a t h).trans_lt this
       · exact (pos_lt_pos_atom _ hc' h).trans this
     · simp only [Address.pos_nearLitter]
-      by_cases h : t = typedNearLitter N
-      · subst h
-        rw [pos_typedNearLitter] at this
-        exact this
+      by_cases h : t.set = typedNearLitter N
+      · exact (pos_typedNearLitter N t h).trans_lt this
       · exact (pos_lt_pos_nearLitter _ hc' h).trans this
   case fuzzBot γ _ ε _ hε A a =>
     simp only [Address.pos_atom, Address.pos_nearLitter]

ConNF/FOA/Basic/Hypotheses.lean

@@ -139,11 +139,11 @@ class FOAAssumptions extends FOAData where
   /-- Inflexible litters whose atoms occur in designated supports have position less than the
   original tangle. -/
   pos_lt_pos_atom {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {a : Atom} :
-    ⟨A, Sum.inl a⟩ ∈ t.support → t ≠ typedAtom a → pos a < pos t
+    ⟨A, Sum.inl a⟩ ∈ t.support → t.set ≠ typedAtom a → pos a < pos t
   /-- Inflexible litters touching near-litters in designated supports have position less than the
   original tangle. -/
   pos_lt_pos_nearLitter {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {N : NearLitter} :
-    ⟨A, Sum.inr N⟩ ∈ t.support → t ≠ typedNearLitter N → pos N < pos t
+    ⟨A, Sum.inr N⟩ ∈ t.support → t.set ≠ typedNearLitter N → pos N < pos t
   /-- The `fuzz` map commutes with allowable permutations. -/
   smul_fuzz {β : TypeIndex} [LeLevel β] {γ : TypeIndex} [LtLevel γ] {δ : Λ} [LtLevel δ]
     (hγ : γ < β) (hδ : (δ : TypeIndex) < β) (hγδ : γ ≠ δ) (ρ : Allowable β) (t : Tangle γ) :

ConNF/Fuzz/Hypotheses.lean

@@ -198,10 +198,10 @@ with the conditions given in `BasePositions`, but this requirement is expressed
 class TypedObjects where
   /-- Encode an atom as an `α`-tangle. The resulting model element has a `⊥`-extension which
   contains only this atom. -/
-  typedAtom : Atom ↪ Tangle α
+  typedAtom : Atom ↪ TSet α
   /-- Encode a near-litter as an `α`-tangle. The resulting model element has a `⊥`-extension which
   contains only this near-litter. -/
-  typedNearLitter : NearLitter ↪ Tangle α
+  typedNearLitter : NearLitter ↪ TSet α
   smul_typedNearLitter :
     ∀ (ρ : Allowable α) (N : NearLitter),
     ρ • typedNearLitter N =
@@ -239,13 +239,13 @@ theorem lt_pos_symmDiff [BasePositions] (a : Atom) (N : NearLitter) (h : a ∈ l
   BasePositions.lt_pos_symmDiff a N h
 
 class PositionedObjects [BasePositions] [PositionedTangles α] [TypedObjects α] where
-  pos_typedAtom (a : Atom) : pos (typedAtom a : Tangle α) = pos a
-  pos_typedNearLitter (N : NearLitter) : pos (typedNearLitter N : Tangle α) = pos N
+  pos_typedAtom (a : Atom) (t : Tangle α) :
+    t.set = typedAtom a → pos a ≤ pos t
+  pos_typedNearLitter (N : NearLitter) (t : Tangle α) :
+    t.set = typedNearLitter N → pos N ≤ pos t
 
 export PositionedObjects (pos_typedAtom pos_typedNearLitter)
 
-attribute [simp] pos_typedAtom pos_typedNearLitter
-
 namespace Allowable
 
 variable {α}
@@ -254,7 +254,7 @@ variable [TypedObjects α]
 /-- The action of allowable permutations on tangles commutes with the `typedNearLitter` function
 mapping near-litters to typed near-litters. This can be seen by representing tangles as codes. -/
 theorem smul_typedNearLitter (ρ : Allowable α) (N : NearLitter) :
-    (ρ • typedNearLitter N : Tangle α) =
+    (ρ • typedNearLitter N : TSet α) =
     typedNearLitter ((Allowable.toStructPerm ρ) (Quiver.Hom.toPath <| bot_lt_coe α) • N) :=
   TypedObjects.smul_typedNearLitter _ _
 

ConNF/Model/Construction.lean

@@ -1,6 +1,5 @@
 import ConNF.NewTangle
 import ConNF.Counting
-import ConNF.Model.PretangleEmbedding
 
 open Cardinal Function MulAction Set Sum Quiver WithBot