Theorem: List.exists_subperm_length_eq (LeanCamCombi/Mathlib/Data/List/DropRight.lean)

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hn : n ≤ l.length
⊢ ∃ l', l' <+~ l ∧ l'.length = n
Tactic:
simpa using nil_subperm.exists_intermediate (Nat.zero_le _) hn
State after:
no goals