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

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ l <+: take n l'
Tactic:
rw [hl.eq_take]
State after:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ take l.length l' <+: take n l'

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <+: l'
h : l.length ≤ n
⊢ take l.length l' <+: take n l'
Tactic:
exact take_prefix_take h
State after:
no goals