internlm/Lean-Github huggingface dataset:
Theorem: List.modifyNth_comm_of_comm
Proof state before:
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
cases heq: decide (i = j) with
| true =>
  simp only [decide_eq_true_eq] at heq
  rw [List.modifyNth_modifyNth_eq heq, List.modifyNth_modifyNth_eq (Eq.symm heq), P.comp_eq, heq]
| false =>
  simp only [decide_eq_false_iff_not] at heq
  have heq₂ : j ≠ i := by simp only [ne_eq, ne_comm, heq, not_false_iff]
  rw [List.modifyNth_modifyNth_ne heq, List.modifyNth_modifyNth_ne heq₂]
Proof state after:
no goals
Theorem: List.modifyNth_comm_of_comm
Proof state before:
case true
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : decide (i = j) = true
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
simp only [decide_eq_true_eq] at heq
Proof state after:
case true
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_comm_of_comm
Proof state before:
case true
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [List.modifyNth_modifyNth_eq heq, List.modifyNth_modifyNth_eq (Eq.symm heq), P.comp_eq, heq]
Proof state after:
no goals
Theorem: List.modifyNth_comm_of_comm
Proof state before:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : decide (i = j) = false
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
simp only [decide_eq_false_iff_not] at heq
Proof state after:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_comm_of_comm
Proof state before:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
have heq₂ : j ≠ i := by simp only [ne_eq, ne_comm, heq, not_false_iff]
Proof state after:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
heq₂ : j ≠ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_comm_of_comm
Proof state before:
case false
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
heq₂ : j ≠ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [List.modifyNth_modifyNth_ne heq, List.modifyNth_modifyNth_ne heq₂]
Proof state after:
no goals
Theorem: List.modifyNth_comm_of_comm
Proof state before:
α✝ : Type u_1
f g : α✝ → α✝
i j : ℕ
l : List α✝
P : Function.Commute f g
heq : ¬i = j
⊢ j ≠ i
Tactic:
simp only [ne_eq, ne_comm, heq, not_false_iff]
Proof state after:
no goals
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
l₁ : List α✝
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P l₁)
Tactic:
induction l₁ with
| nil => 
  simp only [nil_append, List.append_eq, splitOnP_nil, modifyLast_singleton]
  apply List.splitOnP_eq_single
  apply h
| cons head tail ih =>
  rw [cons_append, splitOnP_cons, splitOnP_cons]
  split
  case inl heq =>
    rw [ih,modifyLast_cons]
    apply List.splitOnP_ne_nil
  case inr heq =>
    rw [ih, modifyLast_eq_modifyNth, modifyLast_eq_modifyNth,
      modifyHead_eq_modifyNth, modifyHead_eq_modifyNth,
      modifyNth_comm_of_comm]
    simp only [List.append_eq, tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, modify_get?_length]
    simp only [Function.Commute, Function.Semiconj, List.append_eq, cons_append, forall_const]
Proof state after:
no goals
Theorem: List.splitOnP_append
Proof state before:
case nil
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P ([] ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P [])
Tactic:
simp only [nil_append, List.append_eq, splitOnP_nil, modifyLast_singleton]
Proof state after:
case nil
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P l₂ = [l₂]
Theorem: List.splitOnP_append
Proof state before:
case nil
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ splitOnP P l₂ = [l₂]
Tactic:
apply List.splitOnP_eq_single
Proof state after:
case nil.h
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ ∀ (x : α✝), x ∈ l₂ → ¬P x = true
Theorem: List.splitOnP_append
Proof state before:
case nil.h
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
⊢ ∀ (x : α✝), x ∈ l₂ → ¬P x = true
Tactic:
apply h
Proof state after:
no goals
Theorem: List.splitOnP_append
Proof state before:
case cons
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
⊢ splitOnP P (head :: tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P (head :: tail))
Tactic:
rw [cons_append, splitOnP_cons, splitOnP_cons]
Proof state after:
case cons
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
⊢ (if P head = true then [] :: splitOnP P (tail ++ l₂) else modifyHead (cons head) (splitOnP P (tail ++ l₂))) =
    modifyLast (fun x => List.append x l₂)
      (if P head = true then [] :: splitOnP P tail else modifyHead (cons head) (splitOnP P tail))
Theorem: List.splitOnP_append
Proof state before:
case cons
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
⊢ (if P head = true then [] :: splitOnP P (tail ++ l₂) else modifyHead (cons head) (splitOnP P (tail ++ l₂))) =
    modifyLast (fun x => List.append x l₂)
      (if P head = true then [] :: splitOnP P tail else modifyHead (cons head) (splitOnP P tail))
Tactic:
split
Proof state after:
case cons.inl
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
h✝ : P head = true
⊢ [] :: splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) ([] :: splitOnP P tail)

case cons.inr
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
h✝ : ¬P head = true
⊢ modifyHead (cons head) (splitOnP P (tail ++ l₂)) =
    modifyLast (fun x => List.append x l₂) (modifyHead (cons head) (splitOnP P tail))
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ [] :: splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) ([] :: splitOnP P tail)
Tactic:
case inl heq =>
  rw [ih,modifyLast_cons]
  apply List.splitOnP_ne_nil
Proof state after:
no goals
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyHead (cons head) (splitOnP P (tail ++ l₂)) =
    modifyLast (fun x => List.append x l₂) (modifyHead (cons head) (splitOnP P tail))
Tactic:
case inr heq =>
  rw [ih, modifyLast_eq_modifyNth, modifyLast_eq_modifyNth,
    modifyHead_eq_modifyNth, modifyHead_eq_modifyNth,
    modifyNth_comm_of_comm]
  simp only [List.append_eq, tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, modify_get?_length]
  simp only [Function.Commute, Function.Semiconj, List.append_eq, cons_append, forall_const]
Proof state after:
no goals
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ [] :: splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) ([] :: splitOnP P tail)
Tactic:
rw [ih,modifyLast_cons]
Proof state after:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ splitOnP P tail ≠ []
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : P head = true
⊢ splitOnP P tail ≠ []
Tactic:
apply List.splitOnP_ne_nil
Proof state after:
no goals
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyHead (cons head) (splitOnP P (tail ++ l₂)) =
    modifyLast (fun x => List.append x l₂) (modifyHead (cons head) (splitOnP P tail))
Tactic:
rw [ih, modifyLast_eq_modifyNth, modifyLast_eq_modifyNth,
  modifyHead_eq_modifyNth, modifyHead_eq_modifyNth,
  modifyNth_comm_of_comm]
Proof state after:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyNth (fun x => List.append x l₂) (length (splitOnP P tail) - 1) (modifyNth (cons head) 0 (splitOnP P tail)) =
    modifyNth (fun x => List.append x l₂) (length (modifyNth (cons head) 0 (splitOnP P tail)) - 1)
      (modifyNth (cons head) 0 (splitOnP P tail))

α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ modifyNth (fun x => List.append x l₂) (length (splitOnP P tail) - 1) (modifyNth (cons head) 0 (splitOnP P tail)) =
    modifyNth (fun x => List.append x l₂) (length (modifyNth (cons head) 0 (splitOnP P tail)) - 1)
      (modifyNth (cons head) 0 (splitOnP P tail))

α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂
Tactic:
simp only [List.append_eq, tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, modify_get?_length]
Proof state after:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂
Theorem: List.splitOnP_append
Proof state before:
α✝ : Type u_1
l₂ : List α✝
P : α✝ → Bool
h : ∀ (e : α✝), e ∈ l₂ → ¬P e = true
head : α✝
tail : List α✝
ih : splitOnP P (tail ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP P tail)
heq : ¬P head = true
⊢ Function.Commute (cons head) fun x => List.append x l₂
Tactic:
simp only [Function.Commute, Function.Semiconj, List.append_eq, cons_append, forall_const]
Proof state after:
no goals
Theorem: List.splitOn_append
Proof state before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ splitOn delim (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOn delim l₁)
Tactic:
unfold splitOn
Proof state after:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ splitOnP (fun x => x == delim) (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP (fun x => x == delim) l₁)
Theorem: List.splitOn_append
Proof state before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ splitOnP (fun x => x == delim) (l₁ ++ l₂) = modifyLast (fun x => List.append x l₂) (splitOnP (fun x => x == delim) l₁)
Tactic:
rw [List.splitOnP_append]
Proof state after:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
Theorem: List.splitOn_append
Proof state before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
⊢ ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
Tactic:
intro e ein
Proof state after:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
e : α
ein : e ∈ l₂
⊢ ¬(e == delim) = true
Theorem: List.splitOn_append
Proof state before:
α : Type u_1
delim : α
inst✝ : BEq α
l₁ l₂ : List α
h : ∀ (e : α), e ∈ l₂ → ¬(e == delim) = true
e : α
ein : e ∈ l₂
⊢ ¬(e == delim) = true
Tactic:
exact h e ein
Proof state after:
no goals
Theorem: List.modifyHead_append
Proof state before:
α✝ : Type u_1
l₁ : List α✝
f : α✝ → α✝
l₂ : List α✝
h : l₁ ≠ []
⊢ modifyHead f (l₁ ++ l₂) = modifyHead f l₁ ++ l₂
Tactic:
cases l₁ with
| nil => simp only [ne_eq, not_true] at h
| cons head tail => simp only [modifyHead, cons_append]
Proof state after:
no goals
Theorem: List.modifyHead_append
Proof state before:
case nil
α✝ : Type u_1
f : α✝ → α✝
l₂ : List α✝
h : [] ≠ []
⊢ modifyHead f ([] ++ l₂) = modifyHead f [] ++ l₂
Tactic:
simp only [ne_eq, not_true] at h
Proof state after:
no goals
Theorem: List.modifyHead_append
Proof state before:
case cons
α✝ : Type u_1
f : α✝ → α✝
l₂ : List α✝
head : α✝
tail : List α✝
h : head :: tail ≠ []
⊢ modifyHead f (head :: tail ++ l₂) = modifyHead f (head :: tail) ++ l₂
Tactic:
simp only [modifyHead, cons_append]
Proof state after:
no goals
Theorem: List.splitOnP_last
Proof state before:
α : Type u_1
P : α → Bool
inst✝ : BEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P (front ++ sep :: tail) = splitOnP P front ++ [tail]
Tactic:
induction front with
| nil => 
  simp only [nil_append, splitOnP_cons, hsep, modifyHead, ite_true, splitOnP_nil, singleton_append, cons.injEq,
    true_and]
  rw [List.splitOnP_eq_single]
  apply h
| cons hd tl ih =>
  simp only [cons_append, splitOnP_cons]
  split
  . simp only [ih, cons_append]
  . rw [ih, List.modifyHead_append]
    apply List.splitOnP_ne_nil
Proof state after:
no goals
Theorem: List.splitOnP_last
Proof state before:
case nil
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P ([] ++ sep :: tail) = splitOnP P [] ++ [tail]
Tactic:
simp only [nil_append, splitOnP_cons, hsep, modifyHead, ite_true, splitOnP_nil, singleton_append, cons.injEq,
  true_and]
Proof state after:
case nil
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P tail = [tail]
Theorem: List.splitOnP_last
Proof state before:
case nil
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ splitOnP P tail = [tail]
Tactic:
rw [List.splitOnP_eq_single]
Proof state after:
case nil.h
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ ∀ (x : α), x ∈ tail → ¬P x = true
Theorem: List.splitOnP_last
Proof state before:
case nil.h
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
⊢ ∀ (x : α), x ∈ tail → ¬P x = true
Tactic:
apply h
Proof state after:
no goals
Theorem: List.splitOnP_last
Proof state before:
case cons
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
⊢ splitOnP P (hd :: tl ++ sep :: tail) = splitOnP P (hd :: tl) ++ [tail]
Tactic:
simp only [cons_append, splitOnP_cons]
Proof state after:
case cons
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
⊢ (if P hd = true then [] :: splitOnP P (tl ++ sep :: tail)
    else modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail))) =
    (if P hd = true then [] :: splitOnP P tl else modifyHead (cons hd) (splitOnP P tl)) ++ [tail]
Theorem: List.splitOnP_last
Proof state before:
case cons
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
⊢ (if P hd = true then [] :: splitOnP P (tl ++ sep :: tail)
    else modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail))) =
    (if P hd = true then [] :: splitOnP P tl else modifyHead (cons hd) (splitOnP P tl)) ++ [tail]
Tactic:
split
Proof state after:
case cons.inl
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : P hd = true
⊢ [] :: splitOnP P (tl ++ sep :: tail) = [] :: splitOnP P tl ++ [tail]

case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]
Theorem: List.splitOnP_last
Proof state before:
case cons.inl
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : P hd = true
⊢ [] :: splitOnP P (tl ++ sep :: tail) = [] :: splitOnP P tl ++ [tail]

case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]
Tactic:
. simp only [ih, cons_append]
Proof state after:
case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]
Theorem: List.splitOnP_last
Proof state before:
case cons.inr
α : Type u_1
P : α → Bool
inst✝ : BEq α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬P e = true
hsep : P sep = true
hd : α
tl : List α
ih : splitOnP P (tl ++ sep :: tail) = splitOnP P tl ++ [tail]
h✝ : ¬P hd = true
⊢ modifyHead (cons hd) (splitOnP P (tl ++ sep :: tail)) = modifyHead (cons hd) (splitOnP P tl) ++ [tail]
Tactic:
. rw [ih, List.modifyHead_append]
  apply List.splitOnP_ne_nil
Proof state after:
no goals
Theorem: List.splitOn_last
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ splitOn sep (front ++ sep :: tail) = splitOn sep front ++ [tail]
Tactic:
unfold splitOn
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ splitOnP (fun x => x == sep) (front ++ sep :: tail) = splitOnP (fun x => x == sep) front ++ [tail]
Theorem: List.splitOn_last
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ splitOnP (fun x => x == sep) (front ++ sep :: tail) = splitOnP (fun x => x == sep) front ++ [tail]
Tactic:
apply List.splitOnP_last
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ ∀ (e : α), e ∈ tail → ¬(e == sep) = true

case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true
Theorem: List.splitOn_last
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ ∀ (e : α), e ∈ tail → ¬(e == sep) = true

case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true
Tactic:
. exact h
Proof state after:
case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true
Theorem: List.splitOn_last
Proof state before:
case hsep
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
front : List α
sep : α
tail : List α
h : ∀ (e : α), e ∈ tail → ¬(e == sep) = true
⊢ (sep == sep) = true
Tactic:
. simp only [beq_self_eq_true]
Proof state after:
no goals
Theorem: WithTop.untop'_min_left
Proof state before:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : α
y : WithTop α
⊢ untop' d (min (↑x) y) = min x (untop' x y)
Tactic:
cases y with
| none => simp only [none_eq_top, ge_iff_le, le_top, min_eq_left, untop'_coe, untop'_top, min_self]
| some y' => rw [some_eq_coe, ← coe_min, untop'_coe, untop'_coe]
Proof state after:
no goals
Theorem: WithTop.untop'_min_left
Proof state before:
case none
α : Type u_1
d : α
inst✝ : LinearOrder α
x : α
⊢ untop' d (min (↑x) none) = min x (untop' x none)
Tactic:
simp only [none_eq_top, ge_iff_le, le_top, min_eq_left, untop'_coe, untop'_top, min_self]
Proof state after:
no goals
Theorem: WithTop.untop'_min_left
Proof state before:
case some
α : Type u_1
d : α
inst✝ : LinearOrder α
x y' : α
⊢ untop' d (min (↑x) (Option.some y')) = min x (untop' x (Option.some y'))
Tactic:
rw [some_eq_coe, ← coe_min, untop'_coe, untop'_coe]
Proof state after:
no goals
Theorem: WithTop.untop'_min_right
Proof state before:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : WithTop α
y : α
⊢ untop' d (min x ↑y) = min (untop' y x) y
Tactic:
rw [min_comm x, min_comm _ y]
Proof state after:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : WithTop α
y : α
⊢ untop' d (min (↑y) x) = min y (untop' y x)
Theorem: WithTop.untop'_min_right
Proof state before:
α : Type u_1
d : α
inst✝ : LinearOrder α
x : WithTop α
y : α
⊢ untop' d (min (↑y) x) = min y (untop' y x)
Tactic:
apply untop'_min_left
Proof state after:
no goals