Rename Pretangle to StructSet

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

ConNF/Counting/Hypotheses.lean

@@ -1,4 +1,4 @@
-import ConNF.Structural.Pretangle
+import ConNF.Structural.StructSet
 import ConNF.FOA.Basic.Reduction
 
 /-!
@@ -17,43 +17,43 @@ variable [Params.{u}] [Level] [BasePositions]
 
 class CountingAssumptions extends FOAAssumptions where
   /-- Tangles contain only tangles. -/
-  eq_toPretangle_of_mem (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
-    (h : (γ : TypeIndex) < β) (t₁ : TSet β) (t₂ : Pretangle γ) :
-    t₂ ∈ Pretangle.ofCoe (toPretangle t₁) γ h → ∃ t₂' : TSet γ, t₂ = toPretangle t₂'
+  eq_toStructSet_of_mem (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
+    (h : (γ : TypeIndex) < β) (t₁ : TSet β) (t₂ : StructSet γ) :
+    t₂ ∈ StructSet.ofCoe (toStructSet t₁) γ h → ∃ t₂' : TSet γ, t₂ = toStructSet t₂'
   /-- Tangles are extensional at every proper level `γ < β`. -/
-  toPretangle_ext (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) (t₁ t₂ : TSet β) :
-    (∀ t : Pretangle γ,
-      t ∈ Pretangle.ofCoe (toPretangle t₁) γ h ↔ t ∈ Pretangle.ofCoe (toPretangle t₂) γ h) →
-    toPretangle t₁ = toPretangle t₂
+  toStructSet_ext (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) (t₁ t₂ : TSet β) :
+    (∀ t : StructSet γ,
+      t ∈ StructSet.ofCoe (toStructSet t₁) γ h ↔ t ∈ StructSet.ofCoe (toStructSet t₂) γ h) →
+    toStructSet t₁ = toStructSet t₂
   /-- Any `γ`-tangle can be treated as a singleton at level `β` if `γ < β`. -/
   singleton (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
     (h : (γ : TypeIndex) < β) (t : TSet γ) : TSet β
-  singleton_toPretangle (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
+  singleton_toStructSet (β : Λ) [LeLevel β] (γ : Λ) [LeLevel γ]
     (h : (γ : TypeIndex) < β) (t : TSet γ) :
-    Pretangle.ofCoe (toPretangle (singleton β γ h t)) γ h = {toPretangle t}
+    StructSet.ofCoe (toStructSet (singleton β γ h t)) γ h = {toStructSet t}
 
-export CountingAssumptions (eq_toPretangle_of_mem toPretangle_ext
-  singleton singleton_toPretangle)
+export CountingAssumptions (eq_toStructSet_of_mem toStructSet_ext
+  singleton singleton_toStructSet)
 
 variable [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ] (hγ : γ < β)
 
 theorem singleton_smul (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) (t : TSet γ)
     (ρ : Allowable β) :
     ρ • singleton β γ h t = singleton β γ h (Allowable.comp (Hom.toPath h) ρ • t) := by
-  refine toPretangle.inj' ?_
-  refine toPretangle_ext β γ h _ _ ?_
+  refine toStructSet.inj' ?_
+  refine toStructSet_ext β γ h _ _ ?_
   intro u
-  rw [toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
-    singleton_toPretangle, singleton_toPretangle, smul_set_singleton,
-    mem_singleton_iff, mem_singleton_iff, toPretangle_smul, Allowable.toStructPerm_smul,
+  rw [toStructSet_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
+    singleton_toStructSet, singleton_toStructSet, smul_set_singleton,
+    mem_singleton_iff, mem_singleton_iff, toStructSet_smul, Allowable.toStructPerm_smul,
     Allowable.toStructPerm_comp]
 
 theorem singleton_injective (β γ : Λ) [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) :
     Function.Injective (singleton β γ h) := by
   intro t₁ t₂ ht
-  have h₁ := singleton_toPretangle β γ h t₁
-  have h₂ := singleton_toPretangle β γ h t₂
+  have h₁ := singleton_toStructSet β γ h t₁
+  have h₂ := singleton_toStructSet β γ h t₂
   rw [ht, h₂, singleton_eq_singleton_iff] at h₁
-  exact toPretangle.inj' h₁.symm
+  exact toStructSet.inj' h₁.symm
 
 end ConNF

ConNF/Counting/Recode.lean

@@ -66,23 +66,23 @@ theorem smul_raise_eq_iff (c : Address γ) (ρ : Allowable β) :
   simp only [raise_path, raise_value, Address.mk.injEq, true_and]
   rw [Allowable.toStructPerm_comp (Hom.toPath hγ), Tree.comp_apply, raiseIndex]
 
-/-- A set `s` of `γ`-pretangles *appears* at level `α` if it occurs as the `γ`-extension of some
+/-- A set `s` of `γ`-structSets *appears* at level `α` if it occurs as the `γ`-extension of some
 `α`-tangle. -/
-def Appears (s : Set (Pretangle γ)) : Prop :=
-  ∃ t : TSet β, s = Pretangle.ofCoe (toPretangle t) γ hγ
+def Appears (s : Set (StructSet γ)) : Prop :=
+  ∃ t : TSet β, s = StructSet.ofCoe (toStructSet t) γ hγ
 
 /-- Convert a set of `γ`-tangles to the (unique) `α`-tangle with that `γ`-extension,
 if it exists. -/
-noncomputable def toTSet (s : Set (Pretangle γ)) (h : Appears hγ s) : TSet β :=
+noncomputable def toTSet (s : Set (StructSet γ)) (h : Appears hγ s) : TSet β :=
   h.choose
 
-theorem toPretangle_toTSet (s : Set (Pretangle γ)) (h : Appears hγ s) :
-    s = Pretangle.ofCoe (toPretangle (toTSet hγ s h)) γ hγ :=
+theorem toStructSet_toTSet (s : Set (StructSet γ)) (h : Appears hγ s) :
+    s = StructSet.ofCoe (toStructSet (toTSet hγ s h)) γ hγ :=
   h.choose_spec
 
 def AppearsRaised (χs : Set (CodingFunction β)) (U : Support β) : Prop :=
   Appears hγ {u | ∃ χ ∈ χs, ∃ V ≥ U, ∃ hV : V ∈ χ,
-    u ∈ Pretangle.ofCoe (toPretangle ((χ.decode V).get hV)) γ hγ}
+    u ∈ StructSet.ofCoe (toStructSet ((χ.decode V).get hV)) γ hγ}
 
 noncomputable def decodeRaised (χs : Set (CodingFunction β))
     (U : Support β) (hU : AppearsRaised hγ χs U) : TSet β :=
@@ -94,17 +94,17 @@ We now aim to show that `decodeRaised` is a coding function.
 
 theorem decodeRaised_spec (χs : Set (CodingFunction β))
     (U : Support β) (hU : AppearsRaised hγ χs U) :
-    Pretangle.ofCoe (toPretangle (decodeRaised hγ χs U hU)) γ hγ =
+    StructSet.ofCoe (toStructSet (decodeRaised hγ χs U hU)) γ hγ =
     {u | ∃ χ ∈ χs, ∃ V ≥ U, ∃ hV : V ∈ χ,
-      u ∈ Pretangle.ofCoe (toPretangle ((χ.decode V).get hV)) γ hγ} :=
+      u ∈ StructSet.ofCoe (toStructSet ((χ.decode V).get hV)) γ hγ} :=
   hU.choose_spec.symm
 
 theorem appearsRaised_smul {χs : Set (CodingFunction β)}
     (U : Support β) (hU : AppearsRaised hγ χs U) (ρ : Allowable β) :
     AppearsRaised hγ χs (ρ • U) := by
   obtain ⟨t, ht⟩ := hU
   refine ⟨ρ • t, ?_⟩
-  rw [toPretangle_smul, Allowable.toStructPerm_smul, Allowable.toStructPerm_smul,
+  rw [toStructSet_smul, Allowable.toStructPerm_smul, Allowable.toStructPerm_smul,
     StructPerm.ofCoe_smul, ← ht]
   ext u
   constructor
@@ -114,23 +114,23 @@ theorem appearsRaised_smul {χs : Set (CodingFunction β)}
       ?_, by simp only [smul_inv_smul]⟩
     refine ⟨χ, hχ, ρ⁻¹ • V, by rwa [Enumeration.le_inv_iff_smul_le],
       CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
+    rw [CodingFunction.decode_smul, toStructSet_smul, Allowable.toStructPerm_smul,
       StructPerm.ofCoe_smul, map_inv, Tree.comp_inv, smul_mem_smul_set_iff]
     exact hu
   · simp only [ge_iff_le, mem_setOf_eq]
     rintro ⟨u, ⟨χ, hχ, V, hUV, hVχ, hu⟩, rfl⟩
     refine ⟨χ, hχ, ρ • V, Enumeration.smul_le_smul hUV ρ, CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
+    rw [CodingFunction.decode_smul, toStructSet_smul, Allowable.toStructPerm_smul,
       StructPerm.ofCoe_smul, smul_mem_smul_set_iff]
     exact hu
 
 theorem decodeRaised_smul {χs : Set (CodingFunction β)}
     (U : Support β) (hU : AppearsRaised hγ χs U) (ρ : Allowable β) :
     decodeRaised hγ χs (ρ • U) (appearsRaised_smul hγ U hU ρ) = ρ • decodeRaised hγ χs U hU := by
-  refine toPretangle.inj' ?_
-  refine toPretangle_ext β γ hγ _ _ ?_
+  refine toStructSet.inj' ?_
+  refine toStructSet_ext β γ hγ _ _ ?_
   intro u
-  simp_rw [toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
+  simp_rw [toStructSet_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
     decodeRaised_spec]
   -- TODO: Unify this proof with the previous by extracting a lemma.
   constructor
@@ -140,19 +140,19 @@ theorem decodeRaised_smul {χs : Set (CodingFunction β)}
       ?_, by simp only [smul_inv_smul]⟩
     refine ⟨χ, hχ, ρ⁻¹ • V, by rwa [Enumeration.le_inv_iff_smul_le],
       CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
+    rw [CodingFunction.decode_smul, toStructSet_smul, Allowable.toStructPerm_smul,
       StructPerm.ofCoe_smul, map_inv, Tree.comp_inv, smul_mem_smul_set_iff]
     exact hu
   · simp only [ge_iff_le, mem_setOf_eq]
     rintro ⟨u, ⟨χ, hχ, V, hUV, hVχ, hu⟩, rfl⟩
     refine ⟨χ, hχ, ρ • V, Enumeration.smul_le_smul hUV ρ, CodingFunction.smul_mem _ hVχ, ?_⟩
-    rw [CodingFunction.decode_smul, toPretangle_smul, Allowable.toStructPerm_smul,
+    rw [CodingFunction.decode_smul, toStructSet_smul, Allowable.toStructPerm_smul,
       StructPerm.ofCoe_smul, smul_mem_smul_set_iff]
     exact hu
 
 /-- The tangles in the `γ`-extension of a given `β`-tangle. -/
 def tangleExtension (t : TSet β) : Set (TSet γ) :=
-  {u | toPretangle u ∈ Pretangle.ofCoe (toPretangle t) γ hγ}
+  {u | toStructSet u ∈ StructSet.ofCoe (toStructSet t) γ hγ}
 
 /-- A support for a `γ`-tangle, expressed as a set of `β`-support conditions. -/
 noncomputable def raisedSupport (S : Support β) (u : TSet γ) : Support β :=
@@ -216,8 +216,8 @@ theorem raiseSingletons_reducedSupport (S : Support β) (t : TSet β)
     (hSt : Supports (Allowable β) {c | c ∈ S} t) :
     {u | ∃ χ ∈ raiseSingletons hγ S t,
       ∃ V ≥ S, ∃ hV : V ∈ χ,
-      u ∈ Pretangle.ofCoe (toPretangle ((χ.decode V).get hV)) γ hγ} =
-    Pretangle.ofCoe (toPretangle t) γ hγ := by
+      u ∈ StructSet.ofCoe (toStructSet ((χ.decode V).get hV)) γ hγ} =
+    StructSet.ofCoe (toStructSet t) γ hγ := by
   ext u
   constructor
   · simp only [ge_iff_le, mem_setOf_eq, forall_exists_index, and_imp]
@@ -226,21 +226,21 @@ theorem raiseSingletons_reducedSupport (S : Support β) (t : TSet β)
     rw [raiseSingleton, CodingFunction.mem_code] at hVχ
     obtain ⟨ρ, rfl⟩ := hVχ
     simp_rw [CodingFunction.decode_smul, raiseSingleton, CodingFunction.code_decode] at hu
-    rw [Part.get_some, toPretangle_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
-      singleton_toPretangle, smul_set_singleton, mem_singleton_iff] at hu
+    rw [Part.get_some, toStructSet_smul, Allowable.toStructPerm_smul, StructPerm.ofCoe_smul,
+      singleton_toStructSet, smul_set_singleton, mem_singleton_iff] at hu
     subst hu
     rw [← mem_inv_smul_set_iff, Tree.comp_inv, ← StructPerm.ofCoe_smul, ← map_inv,
-      ← Allowable.toStructPerm_smul, ← toPretangle_smul,
+      ← Allowable.toStructPerm_smul, ← toStructSet_smul,
       ← hSt _ (smul_reducedSupport_eq hγ S v ρ hUV), inv_smul_smul]
     exact hv
   · simp only [ge_iff_le, mem_setOf_eq]
     intro hu
-    obtain ⟨u, rfl⟩ := eq_toPretangle_of_mem β γ hγ t u hu
+    obtain ⟨u, rfl⟩ := eq_toStructSet_of_mem β γ hγ t u hu
     refine ⟨_, ⟨u, hu, rfl⟩, raisedSupport hγ S u, ?_⟩
     refine ⟨le_raisedSupport hγ S u, CodingFunction.mem_code_self, ?_⟩
     simp only [raiseSingleton, CodingFunction.mem_code_self, CodingFunction.code_decode,
       Part.get_some]
-    rw [singleton_toPretangle, mem_singleton_iff]
+    rw [singleton_toStructSet, mem_singleton_iff]
 
 theorem appearsRaised_raiseSingletons (S : Support β) (t : TSet β)
     (hSt : Supports (Allowable β) {c | c ∈ S} t) :
@@ -250,8 +250,8 @@ theorem appearsRaised_raiseSingletons (S : Support β) (t : TSet β)
 theorem decodeRaised_raiseSingletons (S : Support β) (t : TSet β)
     (hSt : Supports (Allowable β) {c | c ∈ S} t) :
     decodeRaised hγ (raiseSingletons hγ S t) S (appearsRaised_raiseSingletons hγ S t hSt) = t := by
-  refine toPretangle.inj' ?_
-  refine toPretangle_ext β γ hγ _ _ ?_
+  refine toStructSet.inj' ?_
+  refine toStructSet_ext β γ hγ _ _ ?_
   intro u
   rw [decodeRaised_spec, raiseSingletons_reducedSupport hγ S t hSt]
 

ConNF/Fuzz/Hypotheses.lean

@@ -46,13 +46,13 @@ class TangleData (α : TypeIndex) where
     letI : MulAction Allowable (Address α) :=
       MulAction.compHom _ allowableToStructPerm
     MulAction.Supports Allowable (S : Set (Address α)) t
-  toPretangle : TSet ↪ Pretangle α
-  toPretangle_smul (ρ : Allowable) (t : TSet) :
-    letI : MulAction Allowable (Pretangle α) :=
+  toStructSet : TSet ↪ StructSet α
+  toStructSet_smul (ρ : Allowable) (t : TSet) :
+    letI : MulAction Allowable (StructSet α) :=
       MulAction.compHom _ allowableToStructPerm
-    toPretangle (ρ • t) = ρ • toPretangle t
+    toStructSet (ρ • t) = ρ • toStructSet t
 
-export TangleData (TSet Allowable toPretangle toPretangle_smul)
+export TangleData (TSet Allowable toStructSet toStructSet_smul)
 
 attribute [instance] TangleData.allowableGroup TangleData.allowableAction
 
@@ -148,8 +148,8 @@ instance Bot.tangleData : TangleData ⊥
   allowableToStructPerm_injective := MulEquiv.injective _
   allowableAction := inferInstance
   has_support a := ⟨a.support, a.support_supports⟩
-  toPretangle := Pretangle.ofBot.toEmbedding
-  toPretangle_smul _ _ := rfl
+  toStructSet := StructSet.ofBot.toEmbedding
+  toStructSet_smul _ _ := rfl
 
 @[ext]
 structure TangleCoe (α : Λ) [TangleData α] : Type u where

ConNF/Mathlib/GroupAction.lean

@@ -82,7 +82,7 @@ instance {α : Type _} [∀ i, SMul α <| f i] [∀ i, SMul αᵐᵒᵖ <| f i]
     IsCentralScalar α (∀ i, f i) :=
   ⟨fun _ _ => funext fun _ => op_smul_eq_smul _ _⟩
 
-/-- If `f i` has a faithful scalar action for a given `i`, then so does `Π i, f i`. This is
+/-- If `f i` has a faithful scalar action for a given `i`, then so does `∀ i, f i`. This is
 not an instance as `i` cannot be inferred. -/
 @[to_additive PiProp.has_faithful_vadd_at]
 theorem faithfulSMul_at {α : Type _} [∀ i, SMul α <| f i] [∀ i, Nonempty (f i)] (i : I)

ConNF/Model/Basic.lean

@@ -13,7 +13,7 @@ namespace ConNF
 variable [Params.{u}]
 
 def mem {β α : Λ} (h : β < α) (tβ : TSet β) (tα : TSet α) : Prop :=
-  toPretangle tβ ∈ Pretangle.ofCoe (toPretangle tα) β (coe_lt_coe.mpr h)
+  toStructSet tβ ∈ StructSet.ofCoe (toStructSet tα) β (coe_lt_coe.mpr h)
 
 notation:50 tβ:50 " ∈[" h:50 "] " tα:50 => mem h tβ tα
 
@@ -66,45 +66,45 @@ def mk {β α : Λ} (hβ : β < α) (s : Set (TSet β)) (hs : Symmetric hβ s) :
   letI : LtLevel β := ⟨coe_lt_coe.mpr hβ⟩
   (tSetEquiv α).symm (NewTSet.intro s (tSet_mk_aux hβ s hs))
 
-theorem toPretangle_eq {α : Λ} (t : TSet α) :
-    toPretangle t = letI : Level := ⟨α⟩; NewTSet.toPretangle (tSetEquiv α t) := by
-  rw [← tSetEquiv_toPretangle α t]
+theorem toStructSet_eq {α : Λ} (t : TSet α) :
+    toStructSet t = letI : Level := ⟨α⟩; NewTSet.toStructSet (tSetEquiv α t) := by
+  rw [← tSetEquiv_toStructSet α t]
   rfl
 
 theorem mem_tSetEquiv_iff {β α : Λ} (hβ : β < α) (s : TSet β) (t : TSet α) :
     s ∈[hβ] t ↔
       letI : Level := ⟨α⟩
-      toPretangle s ∈
-        Pretangle.ofCoe (NewTSet.toPretangle (tSetEquiv α t)) β (coe_lt_coe.mpr hβ) := by
-  rw [mem, toPretangle_eq t]
+      toStructSet s ∈
+        StructSet.ofCoe (NewTSet.toStructSet (tSetEquiv α t)) β (coe_lt_coe.mpr hβ) := by
+  rw [mem, toStructSet_eq t]
   rfl
 
-theorem ofCoe_toPretangle_apply_eq {β α : Λ} (hβ : β < α) (t : TSet α) :
-    Pretangle.ofCoe (toPretangle t) β (coe_lt_coe.mpr hβ) =
+theorem ofCoe_toStructSet_apply_eq {β α : Λ} (hβ : β < α) (t : TSet α) :
+    StructSet.ofCoe (toStructSet t) β (coe_lt_coe.mpr hβ) =
     letI : Level := ⟨α⟩
     letI : LtLevel β := ⟨coe_lt_coe.mpr hβ⟩
-    {p | ∃ s ∈ (tSetEquiv α t).val.members β, toPretangle s = p} := by
+    {p | ∃ s ∈ (tSetEquiv α t).val.members β, toStructSet s = p} := by
   letI : Level := ⟨α⟩
   letI : LtLevel β := ⟨coe_lt_coe.mpr hβ⟩
-  rw [toPretangle_eq t, NewTSet.toPretangle]
-  exact congr_fun₂ (Semitangle.toPretangle_ofCoe (tSetEquiv α t).val) β (coe_lt_coe.mpr hβ)
+  rw [toStructSet_eq t, NewTSet.toStructSet]
+  exact congr_fun₂ (Semitangle.toStructSet_ofCoe (tSetEquiv α t).val) β (coe_lt_coe.mpr hβ)
 
 @[simp]
 theorem mem_mk_iff {β α : Λ} (hβ : β < α) (s : Set (TSet β)) (hs : Symmetric hβ s) (t : TSet β) :
     t ∈[hβ] mk hβ s hs ↔ t ∈ s := by
   letI : Level := ⟨α⟩
   letI : LtLevel β := ⟨coe_lt_coe.mpr hβ⟩
   have := NewTSet.intro_members s (tSet_mk_aux hβ s hs)
-  rw [mem, ofCoe_toPretangle_apply_eq hβ]
+  rw [mem, ofCoe_toStructSet_apply_eq hβ]
   simp only [Set.mem_setOf_eq, EmbeddingLike.apply_eq_iff_eq, exists_eq_right]
   rw [mk, Equiv.apply_symm_apply, this]
 
-theorem eq_toPretangle_of_mem {β α : Λ} (hβ : β < α) (t₁ : TSet α) (t₂ : Pretangle β) :
+theorem eq_toStructSet_of_mem {β α : Λ} (hβ : β < α) (t₁ : TSet α) (t₂ : StructSet β) :
     letI : Level := ⟨α⟩
-    t₂ ∈ Pretangle.ofCoe (NewTSet.toPretangle (tSetEquiv α t₁)) β (coe_lt_coe.mpr hβ) →
-    ∃ t₂' : TSet β, t₂ = toPretangle t₂' := by
+    t₂ ∈ StructSet.ofCoe (NewTSet.toStructSet (tSetEquiv α t₁)) β (coe_lt_coe.mpr hβ) →
+    ∃ t₂' : TSet β, t₂ = toStructSet t₂' := by
   intro h
-  simp only [NewTSet.toPretangle, Semitangle.toPretangle, Equiv.apply_symm_apply] at h
+  simp only [NewTSet.toStructSet, Semitangle.toStructSet, Equiv.apply_symm_apply] at h
   obtain ⟨s, _, hs⟩ := h
   exact ⟨s, hs.symm⟩
 
@@ -118,28 +118,28 @@ theorem ext {β α : Λ} (hβ : β < α) (t₁ t₂ : TSet α) :
   simp_rw [TSet.mem_tSetEquiv_iff hβ] at h
   constructor
   · intro hp
-    obtain ⟨s, rfl⟩ := eq_toPretangle_of_mem hβ t₁ p hp
+    obtain ⟨s, rfl⟩ := eq_toStructSet_of_mem hβ t₁ p hp
     exact (h s).mp hp
   · intro hp
-    obtain ⟨s, rfl⟩ := eq_toPretangle_of_mem hβ t₂ p hp
+    obtain ⟨s, rfl⟩ := eq_toStructSet_of_mem hβ t₂ p hp
     exact (h s).mpr hp
 
 theorem smul_mem_smul {β α : Λ} (hβ : β < α) (s : TSet β) (t : TSet α) (ρ : Allowable α)
     (h : s ∈[hβ] t) :
     cons hβ ρ • s ∈[hβ] ρ • t := by
   letI : Level := ⟨α⟩
   letI : LtLevel β := ⟨coe_lt_coe.mpr hβ⟩
-  rw [mem, ofCoe_toPretangle_apply_eq hβ] at h
+  rw [mem, ofCoe_toStructSet_apply_eq hβ] at h
   obtain ⟨s, hs, hs'⟩ := h
-  cases toPretangle.injective hs'
-  rw [mem, toPretangle_smul, ofCoe_toPretangle_apply_eq hβ]
+  cases toStructSet.injective hs'
+  rw [mem, toStructSet_smul, ofCoe_toStructSet_apply_eq hβ]
   refine ⟨(allowableIso α ρ).val β • s, ?_, ?_⟩
   · rw [tSetEquiv_smul]
     change (allowableIso α ρ).val β • s ∈
       (allowableIso α ρ).val β • (tSetEquiv α t).val.members β
     rw [Set.smul_mem_smul_set_iff]
     exact hs
-  · rw [toPretangle_smul, allowableIso_apply_eq (coe_lt_coe.mpr hβ)]
+  · rw [toStructSet_smul, allowableIso_apply_eq (coe_lt_coe.mpr hβ)]
     rfl
 
 theorem smul_mem_smul_iff {β α : Λ} (hβ : β < α) (s : TSet β) (t : TSet α) (ρ : Allowable α) :