exact ⟨l₁, h⟩
case h.h.intro
α : Type u_1
s t : Multiset α
n : ℕ
l₀ : List α
hs : card ⟦l₀⟧ ≤ n
l₂ : List α
ht : n ≤ card ⟦l₂⟧
hst : ⟦l₀⟧ ≤ ⟦l₂⟧
l₁ : List α
h : l₀.Subperm l₁ ∧ l₁.Subperm l₂ ∧ l₁.length = n
⊢ ∃ u, ⟦l₀⟧ ≤ u ∧ u ≤ ⟦l₂⟧ ∧ card u = n
no goals