no goals
α : Type u
n : ℕ
h : n ≤ length []
⊢ rotate' [] n = drop n [] ++ take n []
simp [drop_append_of_le_length h]
no goals
α : Type u
l : List α
h : 0 ≤ length l
⊢ rotate' l 0 = drop 0 l ++ take 0 l
simp [take_append_of_le_length h]
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
have hnl : n ≤ l.length := le_of_succ_le_succ h
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
have hnl' : n ≤ (l ++ [a]).length := by
  rw [length_append, length_cons, List.length]; exact le_of_succ_le h
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ rotate' (a :: l) (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take,
    drop_append_of_le_length hnl, take_append_of_le_length hnl]
no goals
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
hnl' : n ≤ length (l ++ [a])
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
simp
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length l + succ 0
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length (l ++ [a])
rw [length_append, length_cons, List.length]
no goals
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ length (a :: l)
hnl : n ≤ length l
⊢ n ≤ length l + succ 0
exact le_of_succ_le h