-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_reverse {α} {xs : List α} {n : Nat} :
    xs.reverse.take n = (xs.drop (xs.length - n)).reverse

Proof state:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length

Tactic:
rw [length_append, length_reverse]

Result:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ xs_tl.length + 1 = xs_tl.length + [xs_hd].length

Proof state:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

Tactic:
have w : xs.length - n = 0 := by omega

Result:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
w : xs.length - n = 0
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

Proof state:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
w : xs.length - n = 0
⊢ xs.length ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ take (xs_tl.length + 1) (xs_tl.reverse ++ [xs_hd]) = (xs_hd :: xs_tl).reverse

Tactic:
suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
  rw [this, take_length, reverse_cons]

Result:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length

Proof state:
α : Type u_1
xs : List α
n : Nat
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

Tactic:
by_cases h : n ≤ xs.length

Result:
case pos
α : Type u_1
xs : List α
n : Nat
h : n ≤ xs.length
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

Proof state:
case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h' : n < (xs_hd :: xs_tl).length
⊢ take n (xs_tl.reverse ++ [xs_hd]) = (drop (xs_tl.length + 1 - n) (xs_hd :: xs_tl)).reverse

Tactic:
have h' := Nat.le_of_succ_le_succ h'

Result:
case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ take n (xs_tl.reverse ++ [xs_hd]) = (drop (xs_tl.length + 1 - n) (xs_hd :: xs_tl)).reverse

Proof state:
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
⊢ xs.length - n = 0

Tactic:
omega

Result:
no goals

Proof state:
case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ (drop (xs_tl.length - n) xs_tl).reverse = (drop (xs_tl.length + 1 - n) (xs_hd :: xs_tl)).reverse

case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ n ≤ xs_tl.reverse.length

Tactic:
rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]

Result:
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ xs_tl.length + 1 - n = (xs_tl.length - n).succ

case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ n ≤ xs_tl.reverse.length

Proof state:
case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ n ≤ xs_tl.reverse.length

Tactic:
rwa [length_reverse]

Result:
no goals

Proof state:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ take (xs_hd :: xs_tl).length (xs_tl.reverse ++ [xs_hd]) =
    (drop (xs_tl.length + 1 - (xs_hd :: xs_tl).length) (xs_hd :: xs_tl)).reverse

Tactic:
rw [length, Nat.sub_self, drop]

Result:
case inr
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
h : (xs_hd :: xs_tl).length ≤ (xs_hd :: xs_tl).length
⊢ take (xs_tl.length + 1) (xs_tl.reverse ++ [xs_hd]) = (xs_hd :: xs_tl).reverse

Proof state:
case pos
α : Type u_1
xs : List α
n : Nat
h : n ≤ xs.length
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

Tactic:
induction xs generalizing n <;>
  simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]

Result:
case pos.cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {n : Nat}, n ≤ tail✝.length → take n tail✝.reverse = (drop (tail✝.length - n) tail✝).reverse
n : Nat
h : n ≤ (head✝ :: tail✝).length
⊢ take n (tail✝.reverse ++ [head✝]) = (drop (tail✝.length + 1 - n) (head✝ :: tail✝)).reverse

Proof state:
case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ take n (xs_tl.reverse ++ [xs_hd]) = (drop (xs_tl.length + 1 - n) (xs_hd :: xs_tl)).reverse

Tactic:
rw [take_append_of_le_length, xs_ih h']

Result:
case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ (drop (xs_tl.length - n) xs_tl).reverse = (drop (xs_tl.length + 1 - n) (xs_hd :: xs_tl)).reverse

case inl
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ n ≤ xs_tl.reverse.length

Proof state:
α : Type u_1
xs_hd : α
xs_tl : List α
xs_ih : ∀ {n : Nat}, n ≤ xs_tl.length → take n xs_tl.reverse = (drop (xs_tl.length - n) xs_tl).reverse
n : Nat
h : n ≤ (xs_hd :: xs_tl).length
h'✝ : n < (xs_hd :: xs_tl).length
h' : n ≤ xs_tl.length
⊢ xs_tl.length + 1 - n = (xs_tl.length - n).succ

Tactic:
rwa [succ_eq_add_one, Nat.sub_add_comm]

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
w : xs.length - n = 0
⊢ xs.reverse.length ≤ n

Tactic:
simp

Result:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
w : xs.length - n = 0
⊢ xs.length ≤ n

Proof state:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
w : xs.length - n = 0
⊢ take n xs.reverse = (drop (xs.length - n) xs).reverse

Tactic:
rw [take_of_length_le, w, drop_zero]

Result:
case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
w : xs.length - n = 0
⊢ xs.reverse.length ≤ n