ι : Type ?u.157660
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
a : α
l : List α
h : length (a :: l) ≤ n + 1
⊢ a :: take n l = a :: l
ι : Type ?u.157660
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
a : α
l : List α
h : length (a :: l) ≤ n + 1
⊢ take (n + 1) (a :: l) = a :: l
change a :: take n l = a :: l
no goals
ι : Type ?u.157660
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
a : α
l : List α
h : length (a :: l) ≤ n + 1
⊢ a :: take n l = a :: l
rw [take_all_of_le (le_of_succ_le_succ h)]