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

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h : m ≤ n
⊢ take m l <+: take n l
Tactic:
rw [prefix_iff_eq_take, length_take, take_take, min_right_comm, min_eq_left h, take_min]
State after:
no goals