internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.pred (length delim) + Nat.succ (length tl)
Tactic:
calc
  length delim ≤  Nat.pred (length delim) + 1 := by simp only [Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, le_refl, Nat.le_add_of_sub_le]
  _ ≤  Nat.pred (length delim) + Nat.succ (length tl) := by simp only [Nat.succ_eq_add_one, add_le_add_iff_left, le_add_iff_nonneg_left, zero_le, ge_iff_le,
    nonpos_iff_eq_zero]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.pred (length delim) + 1
Tactic:
simp only [Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, le_refl, Nat.le_add_of_sub_le]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ Nat.pred (length delim) + 1 ≤ Nat.pred (length delim) + Nat.succ (length tl)
Tactic:
simp only [Nat.succ_eq_add_one, add_le_add_iff_left, le_add_iff_nonneg_left, zero_le, ge_iff_le,
nonpos_iff_eq_zero]
Proof state after:
no goals
Theorem: List.splitOnList_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim front rest : List α
h₁ : ¬delim <:+: front ++ dropLast delim
⊢ splitOnList delim (front ++ delim ++ rest) = [front] ++ splitOnList delim rest
Tactic:
unfold splitOnList
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim front rest : List α
h₁ : ¬delim <:+: front ++ dropLast delim
⊢ (match delim with
    | [] => [front ++ delim ++ rest]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList
          (splitOnListAux (head :: tail) (front ++ delim ++ rest) #[] #[] (_ : ¬head :: tail = [])))) =
    [front] ++
      match delim with
      | [] => [rest]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))
Theorem: List.splitOnList_progress
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim front rest : List α
h₁ : ¬delim <:+: front ++ dropLast delim
⊢ (match delim with
    | [] => [front ++ delim ++ rest]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList
          (splitOnListAux (head :: tail) (front ++ delim ++ rest) #[] #[] (_ : ¬head :: tail = [])))) =
    [front] ++
      match delim with
      | [] => [rest]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))
Tactic:
cases delim with
| nil =>
  simp only [dropLast, append_nil, nil_isInfix, not_true] at h₁
| cons head tail=>
  simp only
  rw [List.splitOnListAux_progress]
  simp only [Array.toList_eq, Array.map_data, Array.append_data, Array.data_toArray, singleton_append]
  simp only [map, Array.toList_eq, Array.data_toArray]
  exact h₁
Proof state after:
no goals
Theorem: List.splitOnList_progress
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
h₁ : ¬[] <:+: front ++ dropLast []
⊢ (match [] with
    | [] => [front ++ [] ++ rest]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList
          (splitOnListAux (head :: tail) (front ++ [] ++ rest) #[] #[] (_ : ¬head :: tail = [])))) =
    [front] ++
      match [] with
      | [] => [rest]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))
Tactic:
simp only [dropLast, append_nil, nil_isInfix, not_true] at h₁
Proof state after:
no goals
Theorem: List.splitOnList_progress
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ (match head :: tail with
    | [] => [front ++ head :: tail ++ rest]
    | head_1 :: tail_1 =>
      Array.toList
        (Array.map Array.toList
          (splitOnListAux (head_1 :: tail_1) (front ++ head :: tail ++ rest) #[] #[] (_ : ¬head_1 :: tail_1 = [])))) =
    [front] ++
      match head :: tail with
      | [] => [rest]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))
Tactic:
simp only
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ Array.toList
      (Array.map Array.toList
        (splitOnListAux (head :: tail) (front ++ head :: tail ++ rest) #[] #[] (_ : ¬head :: tail = []))) =
    [front] ++
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))
Theorem: List.splitOnList_progress
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ Array.toList
      (Array.map Array.toList
        (splitOnListAux (head :: tail) (front ++ head :: tail ++ rest) #[] #[] (_ : ¬head :: tail = []))) =
    [front] ++
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))
Tactic:
rw [List.splitOnListAux_progress]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ Array.toList
      (Array.map Array.toList
        (#[toArray front] ++ splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = []))) =
    [front] ++
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Theorem: List.splitOnList_progress
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ Array.toList
      (Array.map Array.toList
        (#[toArray front] ++ splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = []))) =
    [front] ++
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])))

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Tactic:
simp only [Array.toList_eq, Array.map_data, Array.append_data, Array.data_toArray, singleton_append]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ map Array.toList (toArray front :: (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])).data) =
    front :: map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])).data

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Theorem: List.splitOnList_progress
Proof state before:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ map Array.toList (toArray front :: (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])).data) =
    front :: map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])).data

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Tactic:
simp only [map, Array.toList_eq, Array.data_toArray]
Proof state after:
case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Theorem: List.splitOnList_progress
Proof state before:
case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Tactic:
exact h₁
Proof state after:
no goals
Theorem: List.join_intersperse_nil
Proof state before:
α : Type u_1
l : List (List α)
⊢ join (intersperse [] l) = join l
Tactic:
match l with
| [] => simp only [join]
| [a] => simp only [join, append_nil]
| a :: b :: tail =>
  simp only [join, List.join_intersperse_nil, nil_append]
Proof state after:
no goals
Theorem: List.join_intersperse_nil
Proof state before:
α : Type u_1
l : List (List α)
⊢ join (intersperse [] []) = join []
Tactic:
simp only [join]
Proof state after:
no goals
Theorem: List.join_intersperse_nil
Proof state before:
α : Type u_1
l : List (List α)
a : List α
⊢ join (intersperse [] [a]) = join [a]
Tactic:
simp only [join, append_nil]
Proof state after:
no goals
Theorem: List.join_intersperse_nil
Proof state before:
α : Type u_1
l : List (List α)
a b : List α
tail : List (List α)
⊢ join (intersperse [] (a :: b :: tail)) = join (a :: b :: tail)
Tactic:
simp only [join, List.join_intersperse_nil, nil_append]
Proof state after:
no goals
Theorem: Array.modify_data
Proof state before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
⊢ (modify a i f).data = List.modifyNth f i a.data
Tactic:
unfold modify Id.run modifyM
Proof state after:
α : Type u_1
a : Array α
i : ℕ
f : α → α
⊢ (if h : i < size a then
        let idx := { val := i, isLt := h };
        let v := get a idx;
        do
        let v ← f v
        pure (set a idx v)
      else pure a).data =
    List.modifyNth f i a.data
Theorem: Array.modify_data
Proof state before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
⊢ (if h : i < size a then
        let idx := { val := i, isLt := h };
        let v := get a idx;
        do
        let v ← f v
        pure (set a idx v)
      else pure a).data =
    List.modifyNth f i a.data
Tactic:
split
Proof state after:
case inl
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : i < size a
⊢ (let idx := { val := i, isLt := h✝ };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyNth f i a.data

case inr
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Theorem: Array.modify_data
Proof state before:
case inl
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : i < size a
⊢ (let idx := { val := i, isLt := h✝ };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyNth f i a.data

case inr
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
. simp
  rw [List.modifyNth_eq_set_get]
  congr 1
Proof state after:
case inr
α : Type u_1
a : Array α
i : ℕ
f : α → α
h✝ : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Theorem: Array.modify_data
Proof state before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
case inr heq =>
  simp at heq
  rw [List.modifyNth_eq_set_get?]
  simp [List.get?_eq_none.2 heq]
Proof state after:
no goals
Theorem: Array.modify_data
Proof state before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : ¬i < size a
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
simp at heq
Proof state after:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = List.modifyNth f i a.data
Theorem: Array.modify_data
Proof state before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = List.modifyNth f i a.data
Tactic:
rw [List.modifyNth_eq_set_get?]
Proof state after:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = Option.getD ((fun a_1 => List.set a.data i (f a_1)) <$> List.get? a.data i) a.data
Theorem: Array.modify_data
Proof state before:
α : Type u_1
a : Array α
i : ℕ
f : α → α
heq : size a ≤ i
⊢ (pure a).data = Option.getD ((fun a_1 => List.set a.data i (f a_1)) <$> List.get? a.data i) a.data
Tactic:
simp [List.get?_eq_none.2 heq]
Proof state after:
no goals
Theorem: List.modifyLast_nil
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
⊢ modifyLast f [] = []
Tactic:
unfold modifyLast modifyLast.go
Proof state after:
α✝ : Type u_1
f : α✝ → α✝
⊢ [] = []
Theorem: List.modifyLast_nil
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
⊢ [] = []
Tactic:
simp only
Proof state after:
no goals
Theorem: List.modifyNth_nil
Proof state before:
α✝ : Type u_1
f : α✝ → α✝
i : ℕ
⊢ modifyNth f i [] = []
Tactic:
simp [List.modifyNth_eq_set]
Proof state after:
no goals
Theorem: List.modifyLast_cons
Proof state before:
α : Type u_1
f : α → α
head : α
tail : List α
h : tail ≠ []
⊢ modifyLast f (head :: tail) = head :: modifyLast f tail
Tactic:
rw [← List.dropLast_append_getLast (List.cons_ne_nil head tail),← List.dropLast_append_getLast h,
 List.modifyLast_append_one, List.modifyLast_append_one]
Proof state after:
α : Type u_1
f : α → α
head : α
tail : List α
h : tail ≠ []
⊢ dropLast (head :: (dropLast tail ++ [getLast tail h])) ++
      [f
          (getLast (head :: (dropLast tail ++ [getLast tail h]))
            (_ : head :: (dropLast tail ++ [getLast tail h]) ≠ []))] =
    head :: (dropLast tail ++ [f (getLast tail h)])
Theorem: List.modifyLast_cons
Proof state before:
α : Type u_1
f : α → α
head : α
tail : List α
h : tail ≠ []
⊢ dropLast (head :: (dropLast tail ++ [getLast tail h])) ++
      [f
          (getLast (head :: (dropLast tail ++ [getLast tail h]))
            (_ : head :: (dropLast tail ++ [getLast tail h]) ≠ []))] =
    head :: (dropLast tail ++ [f (getLast tail h)])
Tactic:
simp only [append_eq_nil, and_false, IsEmpty.forall_iff, dropLast_concat, ne_eq, not_false_iff, getLast_cons,
  getLast_append, cons_append, dropLast]
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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)]
Proof 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 ≠ [])])
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof 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
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof 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
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof 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
Theorem: List.modifyLast_eq_modifyNth
Proof 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
Proof 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
Theorem: List.modifyLast_eq_modifyNth
Proof 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
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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]
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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
Proof state after:
no goals
Theorem: List.modifyLast_eq_modifyNth
Proof 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
Proof 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