internlm/Lean-Github huggingface dataset:
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
⊢ (if h : 0 < size a then
        let idx := { val := 0, isLt := h };
        let v := get a idx;
        do
        let v ← f v
        pure (set a idx v)
      else pure a).data =
    List.modifyHead f a.data
Tactic:
split
Proof state after:
case inl
α : Type u_1
f : α → α
a : Array α
h✝ : 0 < size a
⊢ (let idx := { val := 0, isLt := h✝ };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyHead f a.data

case inr
α : Type u_1
f : α → α
a : Array α
h✝ : ¬0 < size a
⊢ (pure a).data = List.modifyHead f a.data
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ (let idx := { val := 0, isLt := heq };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyHead f a.data
Tactic:
case inl heq =>
  simp [List.set_eq_take_cons_drop _ heq]
  split
  case h_1 heq₂ =>
    apply_fun (@List.toArray α) at heq₂
    simp only [toArray_data] at heq₂
    subst heq₂
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, size_toArray, List.length_nil, lt_self_iff_false] at heq
  case h_2 head tail heq₂ =>
    apply_fun (@List.toArray α) at heq₂
    simp only [toArray_data] at heq₂
    subst heq₂
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, data_toArray, List.tail_cons, List.cons.injEq, and_true]
    congr
    simp [Array.getElem_eq_data_get, Array.data_toArray (head::tail)] 
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get_eq_iff, data_toArray, List.cons.injEq,
      forall_true_left, and_imp, forall_apply_eq_imp_iff', forall_eq', List.get?_zero, List.head?_cons]
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : ¬0 < size a
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
case inr heq =>
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, not_lt] at heq
  rw [← Array.toArray_data a, Array.size_toArray, List.length_eq_zero] at heq
  simp only [Id.pure_eq, heq, List.modifyHead]
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ (let idx := { val := 0, isLt := heq };
      let v := get a idx;
      do
      let v ← f v
      pure (set a idx v)).data =
    List.modifyHead f a.data
Tactic:
simp [List.set_eq_take_cons_drop _ heq]
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ f a[0] :: List.tail a.data =
    match a.data with
    | [] => []
    | a :: l => f a :: l
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
⊢ f a[0] :: List.tail a.data =
    match a.data with
    | [] => []
    | a :: l => f a :: l
Tactic:
split
Proof state after:
case h_1
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq✝ : a.data = []
⊢ f a[0] :: List.tail a.data = []

case h_2
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝¹ : List α
x✝ : α
xs✝ : List α
heq✝ : a.data = x✝ :: xs✝
⊢ f a[0] :: List.tail a.data = f x✝ :: xs✝
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a.data = []
⊢ f a[0] :: List.tail a.data = []
Tactic:
case h_1 heq₂ =>
  apply_fun (@List.toArray α) at heq₂
  simp only [toArray_data] at heq₂
  subst heq₂
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, size_toArray, List.length_nil, lt_self_iff_false] at heq
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a.data = head :: tail
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
case h_2 head tail heq₂ =>
  apply_fun (@List.toArray α) at heq₂
  simp only [toArray_data] at heq₂
  subst heq₂
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, data_toArray, List.tail_cons, List.cons.injEq, and_true]
  congr
  simp [Array.getElem_eq_data_get, Array.data_toArray (head::tail)] 
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get_eq_iff, data_toArray, List.cons.injEq,
    forall_true_left, and_imp, forall_apply_eq_imp_iff', forall_eq', List.get?_zero, List.head?_cons]
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a.data = []
⊢ f a[0] :: List.tail a.data = []
Tactic:
apply_fun (@List.toArray α) at heq₂
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : List.toArray a.data = #[]
⊢ f a[0] :: List.tail a.data = []
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : List.toArray a.data = #[]
⊢ f a[0] :: List.tail a.data = []
Tactic:
simp only [toArray_data] at heq₂
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a = #[]
⊢ f a[0] :: List.tail a.data = []
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
heq₂ : a = #[]
⊢ f a[0] :: List.tail a.data = []
Tactic:
subst heq₂
Proof state after:
α : Type u_1
f : α → α
x✝ : List α
heq : 0 < size #[]
⊢ f #[][0] :: List.tail #[].data = []
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
x✝ : List α
heq : 0 < size #[]
⊢ f #[][0] :: List.tail #[].data = []
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, size_toArray, List.length_nil, lt_self_iff_false] at heq
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a.data = head :: tail
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
apply_fun (@List.toArray α) at heq₂
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : List.toArray a.data = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : List.toArray a.data = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
simp only [toArray_data] at heq₂
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : 0 < size a
x✝ : List α
head : α
tail : List α
heq₂ : a = List.toArray (head :: tail)
⊢ f a[0] :: List.tail a.data = f head :: tail
Tactic:
subst heq₂
Proof state after:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] :: List.tail (List.toArray (head :: tail)).data = f head :: tail
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] :: List.tail (List.toArray (head :: tail)).data = f head :: tail
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, data_toArray, List.tail_cons, List.cons.injEq, and_true]
Proof state after:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] = f head
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ f (List.toArray (head :: tail))[0] = f head
Tactic:
congr
Proof state after:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ (List.toArray (head :: tail))[0] = head
Theorem: Array.modifyHead_data
Proof state before:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ (List.toArray (head :: tail))[0] = head
Tactic:
simp [Array.getElem_eq_data_get, Array.data_toArray (head::tail)]
Proof state after:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ List.get (List.toArray (head :: tail)).data
      { val := 0, isLt := (_ : ↑{ val := 0, isLt := heq } < size (List.toArray (head :: tail))) } =
    head
Theorem: Array.modifyHead_data
Proof state before:
case e_a
α : Type u_1
f : α → α
x✝ : List α
head : α
tail : List α
heq : 0 < size (List.toArray (head :: tail))
⊢ List.get (List.toArray (head :: tail)).data
      { val := 0, isLt := (_ : ↑{ val := 0, isLt := heq } < size (List.toArray (head :: tail))) } =
    head
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get_eq_iff, data_toArray, List.cons.injEq,
  forall_true_left, and_imp, forall_apply_eq_imp_iff', forall_eq', List.get?_zero, List.head?_cons]
Proof state after:
no goals
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : ¬0 < size a
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, not_lt] at heq
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : size a = 0
⊢ (pure a).data = List.modifyHead f a.data
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : size a = 0
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
rw [← Array.toArray_data a, Array.size_toArray, List.length_eq_zero] at heq
Proof state after:
α : Type u_1
f : α → α
a : Array α
heq : a.data = []
⊢ (pure a).data = List.modifyHead f a.data
Theorem: Array.modifyHead_data
Proof state before:
α : Type u_1
f : α → α
a : Array α
heq : a.data = []
⊢ (pure a).data = List.modifyHead f a.data
Tactic:
simp only [Id.pure_eq, heq, List.modifyHead]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim l : List α
acc : Array α
h : delim ≠ []
⊢ splitOnListAux delim l acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l #[] #[] h)
Tactic:
induction l using List.induction_by_length_on generalizing acc with
| h l ih =>
  unfold splitOnListAux
  split
  case h_1 heq =>
    simp [Array.ext_iff]
  case h_2 head tail =>
    split
    case h_1 heq =>
      rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
      . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
        cases (splitOnListAux delim tail #[] #[] h).data with
        | nil => simp only
        | cons => 
          simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
            Array.data_toArray, nil_append, and_self]
      . simp only [length_cons, Nat.lt_succ_self]
      . simp only [length_cons, Nat.lt_succ_self]
    case h_2 heq =>
      have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
      have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
      rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
      simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
acc : Array α
⊢ splitOnListAux delim l acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l #[] #[] h)
Tactic:
unfold splitOnListAux
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
acc : Array α
⊢ (match _h₀ : l with
    | [] => Array.push #[] acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (match _h₀ : l with
      | [] => Array.push #[] #[]
      | head :: tail =>
        match h : getRest l delim with
        | none => splitOnListAux delim tail (Array.push #[] head) #[] h
        | some rest =>
          let_fun x := (_ : sizeOf rest < sizeOf l);
          splitOnListAux delim rest #[] (Array.push #[] #[]) h)
Theorem: List.splitOnListAux_acc
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
acc : Array α
⊢ (match _h₀ : l with
    | [] => Array.push #[] acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (match _h₀ : l with
      | [] => Array.push #[] #[]
      | head :: tail =>
        match h : getRest l delim with
        | none => splitOnListAux delim tail (Array.push #[] head) #[] h
        | some rest =>
          let_fun x := (_ : sizeOf rest < sizeOf l);
          splitOnListAux delim rest #[] (Array.push #[] #[]) h)
Tactic:
split
Proof state after:
case h.h_1
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ Array.push #[] acc = Array.modifyHead (Array.append acc) (Array.push #[] #[])

case h.h_2
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head✝ : α
tail✝ : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head✝ :: tail✝) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ (match h : getRest (head✝ :: tail✝) delim with
    | none => splitOnListAux delim tail✝ (Array.push acc head✝) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head✝ :: tail✝));
      splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (match h : getRest (head✝ :: tail✝) delim with
      | none => splitOnListAux delim tail✝ (Array.push #[] head✝) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head✝ :: tail✝));
        splitOnListAux delim rest #[] (Array.push #[] #[]) h)
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
heq : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ Array.push #[] acc = Array.modifyHead (Array.append acc) (Array.push #[] #[])
Tactic:
case h_1 heq =>
  simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (match h : getRest (head :: tail) delim with
      | none => splitOnListAux delim tail (Array.push #[] head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
        splitOnListAux delim rest #[] (Array.push #[] #[]) h)
Tactic:
case h_2 head tail =>
  split
  case h_1 heq =>
    rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
    . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
      cases (splitOnListAux delim tail #[] #[] h).data with
      | nil => simp only
      | cons => 
        simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
          Array.data_toArray, nil_append, and_self]
    . simp only [length_cons, Nat.lt_succ_self]
    . simp only [length_cons, Nat.lt_succ_self]
  case h_2 heq =>
    have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
    have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
    rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
    simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
heq : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ Array.push #[] acc = Array.modifyHead (Array.append acc) (Array.push #[] #[])
Tactic:
simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (match h : getRest (head :: tail) delim with
      | none => splitOnListAux delim tail (Array.push #[] head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
        splitOnListAux delim rest #[] (Array.push #[] #[]) h)
Tactic:
split
Proof state after:
case h_1
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq✝ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) #[] h =
    Array.modifyHead (Array.append acc) (splitOnListAux delim tail (Array.push #[] head) #[] h)

case h_2
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq✝ : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) #[] h =
    Array.modifyHead (Array.append acc) (splitOnListAux delim tail (Array.push #[] head) #[] h)
Tactic:
case h_1 heq =>
  rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
  . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
    cases (splitOnListAux delim tail #[] #[] h).data with
    | nil => simp only
    | cons => 
      simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
        Array.data_toArray, nil_append, and_self]
  . simp only [length_cons, Nat.lt_succ_self]
  . simp only [length_cons, Nat.lt_succ_self]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
case h_2 heq =>
  have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
  have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
  rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
  simp [Array.ext_iff]
Proof state after:
no goals
Theorem: List.splitOnListAux_acc
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) #[] h =
    Array.modifyHead (Array.append acc) (splitOnListAux delim tail (Array.push #[] head) #[] h)
Tactic:
rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push acc head)) (splitOnListAux delim tail #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim tail #[] #[] h))

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)