stackSize_𝔘₃_le_𝔐

lemma stackSize_𝔘₃_le_𝔐 (x : X) : stackSize (𝔘₃ k n j) x ≤ stackSize (𝔐 k n) x := by  classical  let mf' : 𝔓 X → 𝔓 X := fun u ↦ if mu : u ∈ 𝔘₃ k n j then mf k n j ⟨u, mu⟩ else default  simp_rw [stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id]  refine Finset.card_le_card_of_injOn mf' (fun u mu ↦ ?_) (fun u mu u' mu' e ↦ ?_)  · rw [Finset.coe_filter, mem_setOf, Finset.mem_filter_univ] at mu ⊢    simp_rw [mf', mu.1, dite_true]    have hu : 𝓘 u ≤ 𝓘 (mf k n j ⟨u, mu.1⟩) := (exists_smul_le_of_𝔘₃ ⟨u, mu.1⟩).choose_spec.1    exact ⟨(mf k n j ⟨u, mu.1⟩).2, hu.1 mu.2⟩  · rw [Finset.coe_filter, mem_setOf, Finset.mem_filter_univ] at mu mu'    simp_rw [mf', mu.1, mu'.1, dite_true, Subtype.val_inj] at e    exact congr_arg Subtype.val (mf_injOn mu.2 mu'.2 e)