Theorem: List.modifyLast_eq_modifyNth (One.lean)

State before:
α✝ : Type u_1
f : α✝ → α✝
l : List α✝
⊢ modifyLast f l = modifyNth f (length l - 1) l
Tactic:
cases l with
| nil => simp only [modifyLast_nil, length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_sub, tsub_eq_zero_of_le, modifyNth_nil]
| cons head tail =>
  rw [← List.dropLast_append_getLast (List.cons_ne_nil head tail)]
  simp [List.modifyLast_append_one,List.modifyNth_eq_take_drop, List.take_append_eq_append_take]
  rw [List.take_all_of_le, List.drop_append_eq_append_drop]
  simp only [ne_eq, length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
    nonpos_iff_eq_zero, Nat.sub_self, le_refl, tsub_eq_zero_of_le,
    append_cancel_left_eq, drop]
  split
  case h_1 heq => simp only [ne_eq, append_eq_nil, and_false] at heq
  case h_2 heq => 
    rw [List.drop_eq_nil_of_le] at heq
    simp_all only [tsub_le_iff_right, ge_iff_le, ne_eq, nil_append, cons.injEq]
    simp only [length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
      nonpos_iff_eq_zero, le_refl]
  simp only [length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
    nonpos_iff_eq_zero, le_refl]
State after:
no goals

State before:
case nil
α✝ : Type u_1
f : α✝ → α✝
⊢ modifyLast f [] = modifyNth f (length [] - 1) []
Tactic:
simp only [modifyLast_nil, length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_sub, tsub_eq_zero_of_le, modifyNth_nil]
State after:
no goals

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ modifyLast f (head :: tail) = modifyNth f (length (head :: tail) - 1) (head :: tail)
Tactic:
rw [← List.dropLast_append_getLast (List.cons_ne_nil head tail)]
State after:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ modifyLast f (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])]) =
    modifyNth f (length (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])]) - 1)
      (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])])

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ modifyLast f (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])]) =
    modifyNth f (length (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])]) - 1)
      (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])])
Tactic:
simp [List.modifyLast_append_one,List.modifyNth_eq_take_drop, List.take_append_eq_append_take]
State after:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ dropLast (head :: tail) ++ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] =
    take (length tail) (dropLast (head :: tail)) ++
      match drop (length tail) (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])]) with
      | [] => []
      | a :: l => f a :: l

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ dropLast (head :: tail) ++ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] =
    take (length tail) (dropLast (head :: tail)) ++
      match drop (length tail) (dropLast (head :: tail) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])]) with
      | [] => []
      | a :: l => f a :: l
Tactic:
rw [List.take_all_of_le, List.drop_append_eq_append_drop]
State after:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ dropLast (head :: tail) ++ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] =
    dropLast (head :: tail) ++
      match
        drop (length tail) (dropLast (head :: tail)) ++
          drop (length tail - length (dropLast (head :: tail))) [getLast (head :: tail) (_ : head :: tail ≠ [])] with
      | [] => []
      | a :: l => f a :: l

case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ length (dropLast (head :: tail)) ≤ length tail

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ dropLast (head :: tail) ++ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] =
    dropLast (head :: tail) ++
      match
        drop (length tail) (dropLast (head :: tail)) ++
          drop (length tail - length (dropLast (head :: tail))) [getLast (head :: tail) (_ : head :: tail ≠ [])] with
      | [] => []
      | a :: l => f a :: l

case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
simp only [ne_eq, length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
  nonpos_iff_eq_zero, Nat.sub_self, le_refl, tsub_eq_zero_of_le,
  append_cancel_left_eq, drop]
State after:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] =
    match drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] with
    | [] => []
    | a :: l => f a :: l

case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ length (dropLast (head :: tail)) ≤ length tail

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] =
    match drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] with
    | [] => []
    | a :: l => f a :: l

case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
split
State after:
case cons.h_1
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝ : List α✝
heq✝ : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = []
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = []

case cons.h_2
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq✝ : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = f x✝ :: xs✝

case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ length (dropLast (head :: tail)) ≤ length tail

State before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = []
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = []
Tactic:
case h_1 heq => simp only [ne_eq, append_eq_nil, and_false] at heq
State after:
no goals

State before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = f x✝ :: xs✝
Tactic:
case h_2 heq => 
  rw [List.drop_eq_nil_of_le] at heq
  simp_all only [tsub_le_iff_right, ge_iff_le, ne_eq, nil_append, cons.injEq]
  simp only [length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
    nonpos_iff_eq_zero, le_refl]
State after:
no goals

State before:
case cons
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail : List α✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
simp only [length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
  nonpos_iff_eq_zero, le_refl]
State after:
no goals

State before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = []
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = []
Tactic:
simp only [ne_eq, append_eq_nil, and_false] at heq
State after:
no goals

State before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = f x✝ :: xs✝
Tactic:
rw [List.drop_eq_nil_of_le] at heq
State after:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : [] ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = f x✝ :: xs✝

α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail

State before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : [] ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ [f (getLast (head :: tail) (_ : head :: tail ≠ []))] = f x✝ :: xs✝

α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
simp_all only [tsub_le_iff_right, ge_iff_le, ne_eq, nil_append, cons.injEq]
State after:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail

State before:
α✝ : Type u_1
f : α✝ → α✝
head : α✝
tail x✝¹ : List α✝
x✝ : α✝
xs✝ : List α✝
heq : drop (length tail) (dropLast (head :: tail)) ++ [getLast (head :: tail) (_ : head :: tail ≠ [])] = x✝ :: xs✝
⊢ length (dropLast (head :: tail)) ≤ length tail
Tactic:
simp only [length_dropLast, length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le,
  nonpos_iff_eq_zero, le_refl]
State after:
no goals