exists_smul_le_of_𝔘₃

lemma exists_smul_le_of_𝔘₃ (u : 𝔘₃ k n j) : ∃ m : 𝔐 (X := X) k n, smul 100 u.1 ≤ smul 1 m.1 := by  classical  obtain ⟨u, mu⟩ := u  replace mu := (𝔘₃_subset_𝔘₂.trans 𝔘₂_subset_𝔘₁ |>.trans 𝔘₁_subset_ℭ₁) mu  rw [ℭ₁, mem_sdiff, preℭ₁, mem_setOf, filter_mem_univ_eq_toFinset] at mu  replace mu := (show 0 < 2 ^ j by positivity).trans_le mu.1.2  rw [Finset.card_pos] at mu; obtain ⟨m, hm⟩ := mu  rw [mem_toFinset, 𝔅] at hm; exact ⟨⟨m, hm.1⟩, hm.2⟩