Theorem: List.lastN_eq_reverse_take (One.lean)

State before:
α : Type u_1
n : ℕ
l : List α
⊢ lastN n l = reverse (take n (reverse l))
Tactic:
unfold List.lastN
State after:
α : Type u_1
n : ℕ
l : List α
⊢ drop (length l - n) l = reverse (take n (reverse l))

State before:
α : Type u_1
n : ℕ
l : List α
⊢ drop (length l - n) l = reverse (take n (reverse l))
Tactic:
induction l generalizing n with
| nil => simp only [length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_sub, tsub_eq_zero_of_le, drop_nil,
reverse_nil, take_nil]
| cons head tail ih =>
  simp only [length_cons, tsub_le_iff_right, ge_iff_le, reverse_cons, length_reverse]
  cases h: decide (n ≤ length tail) with
  | false => 
    simp only [decide_eq_false_iff_not, not_le] at h
    rw [Nat.succ_eq_add_one, Nat.add_comm]
    rw [List.take_length_le, List.reverse_append, List.reverse_reverse]
    simp only [tsub_le_iff_right, ge_iff_le, reverse_cons, reverse_nil, nil_append, singleton_append]
    have heq : 1 + length tail - n = 0 := by 
      simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
      rw [Nat.add_comm]
      apply Nat.le_of_lt_succ
      rw [Nat.succ_eq_add_one]
      simp only [add_lt_add_iff_right, h]
    rw [heq]
    simp only [drop]
    rw [List.length_append, List.length_reverse]
    simp only [length_singleton]
    exact h
  | true =>
    simp only [decide_eq_true_eq] at h
    rw [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_sub_assoc, Nat.add_comm, List.drop_cons, ih]
    congr 1
    rw [List.take_append_of_le_length]
    . simp only [length_reverse]; apply h
    . apply h
State after:
no goals

State before:
case nil
α : Type u_1
n : ℕ
⊢ drop (length [] - n) [] = reverse (take n (reverse []))
Tactic:
simp only [length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_sub, tsub_eq_zero_of_le, drop_nil,
reverse_nil, take_nil]
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
⊢ drop (length (head :: tail) - n) (head :: tail) = reverse (take n (reverse (head :: tail)))
Tactic:
simp only [length_cons, tsub_le_iff_right, ge_iff_le, reverse_cons, length_reverse]
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
cases h: decide (n ≤ length tail) with
| false => 
  simp only [decide_eq_false_iff_not, not_le] at h
  rw [Nat.succ_eq_add_one, Nat.add_comm]
  rw [List.take_length_le, List.reverse_append, List.reverse_reverse]
  simp only [tsub_le_iff_right, ge_iff_le, reverse_cons, reverse_nil, nil_append, singleton_append]
  have heq : 1 + length tail - n = 0 := by 
    simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
    rw [Nat.add_comm]
    apply Nat.le_of_lt_succ
    rw [Nat.succ_eq_add_one]
    simp only [add_lt_add_iff_right, h]
  rw [heq]
  simp only [drop]
  rw [List.length_append, List.length_reverse]
  simp only [length_singleton]
  exact h
| true =>
  simp only [decide_eq_true_eq] at h
  rw [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_sub_assoc, Nat.add_comm, List.drop_cons, ih]
  congr 1
  rw [List.take_append_of_le_length]
  . simp only [length_reverse]; apply h
  . apply h
State after:
no goals

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : decide (n ≤ length tail) = false
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
simp only [decide_eq_false_iff_not, not_le] at h
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
rw [Nat.succ_eq_add_one, Nat.add_comm]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
rw [List.take_length_le, List.reverse_append, List.reverse_reverse]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse [head] ++ tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = reverse [head] ++ tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, reverse_cons, reverse_nil, nil_append, singleton_append]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
have heq : 1 + length tail - n = 0 := by 
  simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
  rw [Nat.add_comm]
  apply Nat.le_of_lt_succ
  rw [Nat.succ_eq_add_one]
  simp only [add_lt_add_iff_right, h]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop (1 + length tail - n) (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
rw [heq]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop 0 (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
heq : 1 + length tail - n = 0
⊢ drop 0 (head :: tail) = head :: tail

case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
simp only [drop]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length (reverse tail ++ [head]) ≤ n
Tactic:
rw [List.length_append, List.length_reverse]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + length [head] ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + length [head] ≤ n
Tactic:
simp only [length_singleton]
State after:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n

State before:
case cons.false
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n
Tactic:
exact h
State after:
no goals

State before:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ 1 + length tail - n = 0
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le]
State after:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ 1 + length tail ≤ n

State before:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ 1 + length tail ≤ n
Tactic:
rw [Nat.add_comm]
State after:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n

State before:
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 ≤ n
Tactic:
apply Nat.le_of_lt_succ
State after:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < Nat.succ n

State before:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < Nat.succ n
Tactic:
rw [Nat.succ_eq_add_one]
State after:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < n + 1

State before:
case a
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : length tail < n
⊢ length tail + 1 < n + 1
Tactic:
simp only [add_lt_add_iff_right, h]
State after:
no goals

State before:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : decide (n ≤ length tail) = true
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
simp only [decide_eq_true_eq] at h
State after:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))

State before:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ drop (Nat.succ (length tail) - n) (head :: tail) = reverse (take n (reverse tail ++ [head]))
Tactic:
rw [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_sub_assoc, Nat.add_comm, List.drop_cons, ih]
State after:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ reverse (take n (reverse tail)) = reverse (take n (reverse tail ++ [head]))

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail

State before:
case cons.true
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ reverse (take n (reverse tail)) = reverse (take n (reverse tail ++ [head]))

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
congr 1
State after:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ take n (reverse tail) = take n (reverse tail ++ [head])

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail

State before:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ take n (reverse tail) = take n (reverse tail ++ [head])

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
rw [List.take_append_of_le_length]
State after:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length (reverse tail)

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail

State before:
case cons.true.e_as
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length (reverse tail)

case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
. simp only [length_reverse]; apply h
State after:
case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail

State before:
case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
. apply h
State after:
no goals