Theorem: List.lastN_one_eq_getLast (One.lean)

State before:
α : Type u_1
l : List α
⊢ lastN 1 l = Option.toList (getLast? l)
Tactic:
induction l with
| nil => simp only [length_nil, ge_iff_le, lastN_ge_length, getLast?_nil, Option.to_list_none]
| cons head tail ih=> 
  rw [lastN_cons]
  simp only [length_cons, gt_iff_lt, ge_iff_le]
  split
  case inl heq =>
    have hne: tail ≠ [] := by
      apply List.ne_nil_of_length_pos
      apply Nat.succ_lt_succ_iff.1 heq
    rw [getLast?_cons, ih, getLast?_eq_getLast _ hne, List.getLastD]
    split
    . contradiction
    . simp
  case inr heq =>
    simp at heq
    have hnil: tail = [] := List.eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ heq))
    subst tail
    simp only [getLast?_singleton, Option.to_list_some]
State after:
no goals

State before:
case nil
α : Type u_1
⊢ lastN 1 [] = Option.toList (getLast? [])
Tactic:
simp only [length_nil, ge_iff_le, lastN_ge_length, getLast?_nil, Option.to_list_none]
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ lastN 1 (head :: tail) = Option.toList (getLast? (head :: tail))
Tactic:
rw [lastN_cons]
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if length (head :: tail) > 1 then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if length (head :: tail) > 1 then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))
Tactic:
simp only [length_cons, gt_iff_lt, ge_iff_le]
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if 1 < Nat.succ (length tail) then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
⊢ (if 1 < Nat.succ (length tail) then lastN 1 tail else head :: tail) = Option.toList (getLast? (head :: tail))
Tactic:
split
State after:
case cons.inl
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
h✝ : 1 < Nat.succ (length tail)
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))

case cons.inr
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
h✝ : ¬1 < Nat.succ (length tail)
⊢ head :: tail = Option.toList (getLast? (head :: tail))

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Tactic:
case inl heq =>
  have hne: tail ≠ [] := by
    apply List.ne_nil_of_length_pos
    apply Nat.succ_lt_succ_iff.1 heq
  rw [getLast?_cons, ih, getLast?_eq_getLast _ hne, List.getLastD]
  split
  . contradiction
  . simp
State after:
no goals

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : ¬1 < Nat.succ (length tail)
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
case inr heq =>
  simp at heq
  have hnil: tail = [] := List.eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ heq))
  subst tail
  simp only [getLast?_singleton, Option.to_list_some]
State after:
no goals

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Tactic:
have hne: tail ≠ [] := by
  apply List.ne_nil_of_length_pos
  apply Nat.succ_lt_succ_iff.1 heq
State after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ lastN 1 tail = Option.toList (getLast? (head :: tail))
Tactic:
rw [getLast?_cons, ih, getLast?_eq_getLast _ hne, List.getLastD]
State after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ Option.toList (some (getLast tail hne)) =
    Option.toList
      (some
        (match tail, head with
        | [], a₀ => a₀
        | a :: as, x => getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) [])))

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
hne : tail ≠ []
⊢ Option.toList (some (getLast tail hne)) =
    Option.toList
      (some
        (match tail, head with
        | [], a₀ => a₀
        | a :: as, x => getLast (a :: as) (_ : a :: as = [] → List.noConfusionType False (a :: as) [])))
Tactic:
split
State after:
case h_1
α : Type u_1
head : α
x✝¹ : List α
x✝ : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : 1 < Nat.succ (length [])
hne : [] ≠ []
⊢ Option.toList (some (getLast [] hne)) = Option.toList (some head)

case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))

State before:
case h_1
α : Type u_1
head : α
x✝¹ : List α
x✝ : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : 1 < Nat.succ (length [])
hne : [] ≠ []
⊢ Option.toList (some (getLast [] hne)) = Option.toList (some head)

case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))
Tactic:
. contradiction
State after:
case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))

State before:
case h_2
α : Type u_1
head : α
x✝¹ : List α
x✝ a✝ : α
tail✝ : List α
ih : lastN 1 (a✝ :: tail✝) = Option.toList (getLast? (a✝ :: tail✝))
heq : 1 < Nat.succ (length (a✝ :: tail✝))
hne : a✝ :: tail✝ ≠ []
⊢ Option.toList (some (getLast (a✝ :: tail✝) hne)) =
    Option.toList (some (getLast (a✝ :: tail✝) (_ : a✝ :: tail✝ = [] → List.noConfusionType False (a✝ :: tail✝) [])))
Tactic:
. simp
State after:
no goals

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ tail ≠ []
Tactic:
apply List.ne_nil_of_length_pos
State after:
case a
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ 0 < length tail

State before:
case a
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : 1 < Nat.succ (length tail)
⊢ 0 < length tail
Tactic:
apply Nat.succ_lt_succ_iff.1 heq
State after:
no goals

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : ¬1 < Nat.succ (length tail)
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
simp at heq
State after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
⊢ head :: tail = Option.toList (getLast? (head :: tail))

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
have hnil: tail = [] := List.eq_nil_of_length_eq_zero (Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ heq))
State after:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
hnil : tail = []
⊢ head :: tail = Option.toList (getLast? (head :: tail))

State before:
α : Type u_1
head : α
tail : List α
ih : lastN 1 tail = Option.toList (getLast? tail)
heq : Nat.succ (length tail) ≤ 1
hnil : tail = []
⊢ head :: tail = Option.toList (getLast? (head :: tail))
Tactic:
subst tail
State after:
α : Type u_1
head : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : Nat.succ (length []) ≤ 1
⊢ [head] = Option.toList (getLast? [head])

State before:
α : Type u_1
head : α
ih : lastN 1 [] = Option.toList (getLast? [])
heq : Nat.succ (length []) ≤ 1
⊢ [head] = Option.toList (getLast? [head])
Tactic:
simp only [getLast?_singleton, Option.to_list_some]
State after:
no goals