Prove toPretangle lemmas

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

ConNF/Counting/Conclusions.lean

@@ -53,44 +53,13 @@ theorem TSet.code_injective {β : Λ} [LeLevel β] : Function.Injective (TSet.co
   simp only [← hc, h₁, Enumeration.smul_f] at this
   exact this.symm
 
-theorem mk_tSet_le (β : Λ) [LeLevel β] (hzero : #(CodingFunction 0) < #μ) : #(TSet β) ≤ #μ := by
-  refine (mk_le_of_injective TSet.code_injective).trans ?_
-  simp only [mk_prod, lift_id, mk_support]
-  exact Cardinal.mul_le_of_le (mk_codingFunction β hzero).le le_rfl
-    Params.μ_isStrongLimit.isLimit.aleph0_le
-
-theorem mk_tangle_le (β : Λ) [LeLevel β] : #(Tangle β) ≤ #(TSet β) * #(Support β) := by
-  refine mk_le_of_injective (f := fun t : Tangle β => (t.set, t.support)) ?_
-  intro t₁ t₂ h
-  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
+theorem mk_tSet (β : Λ) [LeLevel β] (hzero : #(CodingFunction 0) < #μ) : #(TSet β) = #μ := 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 (Tangle.typedAtom_injective β)
+  · refine (mk_le_of_injective TSet.code_injective).trans ?_
+    simp only [mk_prod, lift_id, mk_support]
+    exact Cardinal.mul_le_of_le (mk_codingFunction β hzero).le le_rfl
+      Params.μ_isStrongLimit.isLimit.aleph0_le
+  · have := mk_le_of_injective (typedAtom (α := β)).injective
     simp only [mk_atom] at this
     exact this