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

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

Tactic:
simp only [length_reverse, reverse_reverse] at *

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

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

Tactic:
omega

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
⊢ drop n xs.reverse = (take (xs.length - n) xs).reverse

Tactic:
rw [drop_of_length_le, w, take_zero, reverse_nil]

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

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

Tactic:
congr

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

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

Tactic:
rw [take_reverse]

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

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

Tactic:
rw [← reverse_reverse xs] at h

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

Proof state:
α : Type u_1
xs : List α
n : Nat
⊢ drop n xs.reverse = (take (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
⊢ drop n xs.reverse = (take (xs.length - n) xs).reverse

case neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
⊢ drop n xs.reverse = (take (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 pos
α : Type u_1
xs : List α
n : Nat
h : n ≤ xs.length
⊢ drop n xs.reverse = (take (xs.length - n) xs).reverse

Tactic:
conv =>
  rhs
  rw [← reverse_reverse xs]

Result:
case pos
α : Type u_1
xs : List α
n : Nat
h : n ≤ xs.length
⊢ drop n xs.reverse = (take (xs.reverse.reverse.length - n) xs.reverse.reverse).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 neg
α : Type u_1
xs : List α
n : Nat
h : ¬n ≤ xs.length
⊢ drop n xs.reverse = (take (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
⊢ drop n xs.reverse = (take (xs.length - n) xs).reverse

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

Tactic:
generalize xs.reverse = xs' at h ⊢

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