Card t Set le

theorem card_tSet_le (β : TypeIndex) [LeLevel β] :    #(TSet β) ≤ #μ := by  refine (mk_le_of_injective    (f := λ x : TSet β ↦ (Tangle.code      ⟨x, (exists_support x).choose, (exists_support x).choose_spec⟩,      (exists_support x).choose)) ?_).trans ?_  · intro x y h    rw [Prod.mk.injEq, Tangle.code_eq_code_iff] at h    obtain ⟨⟨ρ, hρ⟩, h⟩ := h    have := (exists_support x).choose_spec.supports ρ ?_    · have hρx := congr_arg (·.set) hρ      simp only [Tangle.smul_set] at hρx      rw [← hρx, this]    · have hρx := congr_arg (·.support) hρ      simp only [Tangle.smul_support] at hρx      rw [hρx, h]  · rw [mk_prod, Cardinal.lift_id, Cardinal.lift_id]    apply mul_le_of_le μ_isStrongLimit.aleph0_le (card_codingFunction β).le    rw [card_support]