Theorem: List.lastN_cons (One.lean)

State before:
α : Type u_1
head : α
tail : List α
i : ℕ
⊢ lastN i (head :: tail) = if length (head :: tail) > i then lastN i tail else head :: tail
Tactic:
unfold lastN
State after:
α : Type u_1
head : α
tail : List α
i : ℕ
⊢ drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail

State before:
α : Type u_1
head : α
tail : List α
i : ℕ
⊢ drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
Tactic:
induction tail with
| nil => 
  split
  case inl heq => simp_all
  case inr heq => 
    simp only [length_singleton, gt_iff_lt, Nat.lt_one_iff, ← ne_eq] at heq
    simp only [length_singleton, ge_iff_le, Nat.sub_eq_zero_of_le (Nat.succ_le_of_lt (Nat.pos_of_ne_zero heq)), drop]
| cons mid tail _ih=>
  split
  case inl heq =>
    simp [Nat.succ_eq_one_add]
    rw [Nat.add_sub_assoc, ←Nat.succ_eq_one_add, drop._eq_3]
    simp_all only [Nat.le_of_lt_succ, length_cons, Nat.succ_eq_one_add, ge_iff_le, gt_iff_lt]
  case inr heq =>
    simp only [length_cons, gt_iff_lt, not_lt] at heq
    simp only [length_cons, ge_iff_le, Nat.sub_eq_zero_of_le heq, drop]
State after:
no goals

State before:
case nil
α : Type u_1
head : α
i : ℕ
⊢ drop (length [head] - i) [head] = if length [head] > i then drop (length [] - i) [] else [head]
Tactic:
split
State after:
case nil.inl
α : Type u_1
head : α
i : ℕ
h✝ : length [head] > i
⊢ drop (length [head] - i) [head] = drop (length [] - i) []

case nil.inr
α : Type u_1
head : α
i : ℕ
h✝ : ¬length [head] > i
⊢ drop (length [head] - i) [head] = [head]

State before:
α : Type u_1
head : α
i : ℕ
heq : length [head] > i
⊢ drop (length [head] - i) [head] = drop (length [] - i) []
Tactic:
case inl heq => simp_all
State after:
no goals

State before:
α : Type u_1
head : α
i : ℕ
heq : ¬length [head] > i
⊢ drop (length [head] - i) [head] = [head]
Tactic:
case inr heq => 
  simp only [length_singleton, gt_iff_lt, Nat.lt_one_iff, ← ne_eq] at heq
  simp only [length_singleton, ge_iff_le, Nat.sub_eq_zero_of_le (Nat.succ_le_of_lt (Nat.pos_of_ne_zero heq)), drop]
State after:
no goals

State before:
α : Type u_1
head : α
i : ℕ
heq : length [head] > i
⊢ drop (length [head] - i) [head] = drop (length [] - i) []
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
head : α
i : ℕ
heq : ¬length [head] > i
⊢ drop (length [head] - i) [head] = [head]
Tactic:
simp only [length_singleton, gt_iff_lt, Nat.lt_one_iff, ← ne_eq] at heq
State after:
α : Type u_1
head : α
i : ℕ
heq : i ≠ 0
⊢ drop (length [head] - i) [head] = [head]

State before:
α : Type u_1
head : α
i : ℕ
heq : i ≠ 0
⊢ drop (length [head] - i) [head] = [head]
Tactic:
simp only [length_singleton, ge_iff_le, Nat.sub_eq_zero_of_le (Nat.succ_le_of_lt (Nat.pos_of_ne_zero heq)), drop]
State after:
no goals

State before:
case cons
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) =
    if length (head :: mid :: tail) > i then drop (length (mid :: tail) - i) (mid :: tail) else head :: mid :: tail
Tactic:
split
State after:
case cons.inl
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
h✝ : length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = drop (length (mid :: tail) - i) (mid :: tail)

case cons.inr
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
h✝ : ¬length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail

State before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = drop (length (mid :: tail) - i) (mid :: tail)
Tactic:
case inl heq =>
  simp [Nat.succ_eq_one_add]
  rw [Nat.add_sub_assoc, ←Nat.succ_eq_one_add, drop._eq_3]
  simp_all only [Nat.le_of_lt_succ, length_cons, Nat.succ_eq_one_add, ge_iff_le, gt_iff_lt]
State after:
no goals

State before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : ¬length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Tactic:
case inr heq =>
  simp only [length_cons, gt_iff_lt, not_lt] at heq
  simp only [length_cons, ge_iff_le, Nat.sub_eq_zero_of_le heq, drop]
State after:
no goals

State before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = drop (length (mid :: tail) - i) (mid :: tail)
Tactic:
simp [Nat.succ_eq_one_add]
State after:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (1 + (1 + length tail) - i) (head :: mid :: tail) = drop (1 + length tail - i) (mid :: tail)

State before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ drop (1 + (1 + length tail) - i) (head :: mid :: tail) = drop (1 + length tail - i) (mid :: tail)
Tactic:
rw [Nat.add_sub_assoc, ←Nat.succ_eq_one_add, drop._eq_3]
State after:
case h
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ i ≤ 1 + length tail

State before:
case h
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : length (head :: mid :: tail) > i
⊢ i ≤ 1 + length tail
Tactic:
simp_all only [Nat.le_of_lt_succ, length_cons, Nat.succ_eq_one_add, ge_iff_le, gt_iff_lt]
State after:
no goals

State before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : ¬length (head :: mid :: tail) > i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Tactic:
simp only [length_cons, gt_iff_lt, not_lt] at heq
State after:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : Nat.succ (Nat.succ (length tail)) ≤ i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail

State before:
α : Type u_1
head : α
i : ℕ
mid : α
tail : List α
_ih :
  drop (length (head :: tail) - i) (head :: tail) =
    if length (head :: tail) > i then drop (length tail - i) tail else head :: tail
heq : Nat.succ (Nat.succ (length tail)) ≤ i
⊢ drop (length (head :: mid :: tail) - i) (head :: mid :: tail) = head :: mid :: tail
Tactic:
simp only [length_cons, ge_iff_le, Nat.sub_eq_zero_of_le heq, drop]
State after:
no goals