Theorem: List.lastN_eq_cons_lastN (One.lean)

State before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: lastN n l = lastN (n + 1) l
Tactic:
unfold lastN
State after:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l

State before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l
Tactic:
have h:  length l - (n + 1) < length l := by
  apply Nat.sub_lt_self
  . simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, add_pos_iff, or_true]
  . simp only [Nat.succ_eq_add_one, P, Nat.succ_le_of_lt]
State after:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l

State before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    drop (length l - (n + 1)) l
Tactic:
conv => 
  right
  rw [List.drop_eq_get_cons  (h:=h)]
State after:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    get l { val := length l - (n + 1), isLt := h } :: drop (length l - (n + 1) + 1) l

State before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ get l { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } :: drop (length l - n) l =
    get l { val := length l - (n + 1), isLt := h } :: drop (length l - (n + 1) + 1) l
Tactic:
congr 2
State after:
case e_head.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } = { val := length l - (n + 1), isLt := h }

case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1

State before:
case e_head.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ { val := length l - 1 - n, isLt := (_ : length l - 1 - n < length l) } = { val := length l - (n + 1), isLt := h }

case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1
Tactic:
. congr 1
  rw [Nat.sub_sub, Nat.add_comm]
State after:
case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1

State before:
case e_tail.e_a
α : Type u_1
n : ℕ
l : List α
P : n < length l
h : length l - (n + 1) < length l
⊢ length l - n = length l - (n + 1) + 1
Tactic:
. rw [← Nat.sub_sub, Nat.sub_add_cancel]
  apply Nat.le_of_add_le_add_right (b:=n)
  rw [Nat.sub_add_cancel]
  . rw [Nat.add_comm, ← Nat.succ_eq_add_one]
    apply Nat.succ_le_of_lt P
  . simp only [P, Nat.le_of_lt]
State after:
no goals

State before:
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ length l - (n + 1) < length l
Tactic:
apply Nat.sub_lt_self
State after:
case h₀
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ 0 < n + 1

case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l

State before:
case h₀
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ 0 < n + 1

case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l
Tactic:
. simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, add_pos_iff, or_true]
State after:
case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l

State before:
case h₁
α : Type u_1
n : ℕ
l : List α
P : n < length l
⊢ n + 1 ≤ length l
Tactic:
. simp only [Nat.succ_eq_add_one, P, Nat.succ_le_of_lt]
State after:
no goals