internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : (Array.push r acc).data = #[].data
⊢ False
Tactic:
simp only [Array.push_data, Array.data_toArray, append_eq_nil, and_false] at contr
Proof state after:
no goals
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case cons
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
⊢ (match _h₀ : head :: tail with
    | [] => Array.push r acc
    | head_1 :: tail_1 =>
      match h : getRest (head :: tail) delim with
      | none => splitOnListAux delim tail_1 (Array.push acc head_1) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
        splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Tactic:
simp only
Proof state after:
case cons
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) r h
    | some rest => splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case cons
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) r h
    | some rest => splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Tactic:
match h: getRest (head::tail) delim with
| none => 
  simp only
  have _ : length tail < Nat.succ (length tail) := by apply Nat.lt_succ_self
  apply List.splitOnListAux_ne_nil tail
| some rest => 
  simp only
  have _ : length rest < Nat.succ (length tail) := by
    have h₂ := List.eq_append_of_getRest h
    replace h₂ := congr_arg List.length h₂
    simp at h₂
    rw[h₂]
    apply Nat.lt_add_of_pos_left
    apply Nat.zero_lt_of_ne_zero
    intro contr
    have contr₂ := List.length_eq_zero.1 contr
    contradiction
  apply List.splitOnListAux_ne_nil rest
Proof state after:
no goals
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
⊢ (match h : none with
    | none => splitOnListAux delim tail (Array.push acc head) r h✝
    | some rest => splitOnListAux delim rest #[] (Array.push r acc) h✝) ≠
    #[]
Tactic:
simp only
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]
Tactic:
have _ : length tail < Nat.succ (length tail) := by apply Nat.lt_succ_self
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
x✝ : length tail < Nat.succ (length tail)
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
x✝ : length tail < Nat.succ (length tail)
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]
Tactic:
apply List.splitOnListAux_ne_nil tail
Proof state after:
no goals
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
⊢ length tail < Nat.succ (length tail)
Tactic:
apply Nat.lt_succ_self
Proof state after:
no goals
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ (match h : some rest with
    | none => splitOnListAux delim tail (Array.push acc head) r h✝
    | some rest_1 => splitOnListAux delim rest_1 #[] (Array.push r acc) h✝) ≠
    #[]
Tactic:
simp only
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]
Tactic:
have _ : length rest < Nat.succ (length tail) := by
  have h₂ := List.eq_append_of_getRest h
  replace h₂ := congr_arg List.length h₂
  simp at h₂
  rw[h₂]
  apply Nat.lt_add_of_pos_left
  apply Nat.zero_lt_of_ne_zero
  intro contr
  have contr₂ := List.length_eq_zero.1 contr
  contradiction
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]
Tactic:
apply List.splitOnListAux_ne_nil rest
Proof state after:
no goals
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ length rest < Nat.succ (length tail)
Tactic:
have h₂ := List.eq_append_of_getRest h
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : head :: tail = delim ++ rest
⊢ length rest < Nat.succ (length tail)
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : head :: tail = delim ++ rest
⊢ length rest < Nat.succ (length tail)
Tactic:
replace h₂ := congr_arg List.length h₂
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : length (head :: tail) = length (delim ++ rest)
⊢ length rest < Nat.succ (length tail)
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : length (head :: tail) = length (delim ++ rest)
⊢ length rest < Nat.succ (length tail)
Tactic:
simp at h₂
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < Nat.succ (length tail)
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < Nat.succ (length tail)
Tactic:
rw[h₂]
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < length delim + length rest
Theorem: List.splitOnListAux_ne_nil
Proof state before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < length delim + length rest
Tactic:
apply Nat.lt_add_of_pos_left
Proof state after:
case h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ 0 < length delim
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ 0 < length delim
Tactic:
apply Nat.zero_lt_of_ne_zero
Proof state after:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length delim ≠ 0
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length delim ≠ 0
Tactic:
intro contr
Proof state after:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
⊢ False
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
⊢ False
Tactic:
have contr₂ := List.length_eq_zero.1 contr
Proof state after:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
contr₂ : delim = []
⊢ False
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
contr₂ : delim = []
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.drop_isInfix
Proof state before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ drop n l <:+: l
Tactic:
exists List.take n l, []
Proof state after:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ take n l ++ drop n l ++ [] = l
Theorem: List.drop_isInfix
Proof state before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ take n l ++ drop n l ++ [] = l
Tactic:
simp only [take_append_drop, append_nil]
Proof state after:
no goals
Theorem: List.drop_isInfix_drop
Proof state before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≥ m
⊢ drop n l <:+: drop m l
Tactic:
rw [← Nat.add_sub_of_le h, add_comm, List.drop_add]
Proof state after:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≥ m
⊢ drop (n - m) (drop m l) <:+: drop m l
Theorem: List.drop_isInfix_drop
Proof state before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≥ m
⊢ drop (n - m) (drop m l) <:+: drop m l
Tactic:
apply List.drop_isInfix
Proof state after:
no goals
Theorem: List.take_isInfix
Proof state before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ take n l <:+: l
Tactic:
exists [], drop n l
Proof state after:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ [] ++ take n l ++ drop n l = l
Theorem: List.take_isInfix
Proof state before:
n : ℕ
α✝ : Type u_1
l : List α✝
⊢ [] ++ take n l ++ drop n l = l
Tactic:
simp only [nil_append, take_append_drop]
Proof state after:
no goals
Theorem: List.take_isInfix_take
Proof state before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≤ m
⊢ take n l <:+: take m l
Tactic:
rw [← Nat.add_sub_of_le h]
Proof state after:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≤ m
⊢ take n l <:+: take (n + (m - n)) l
Theorem: List.take_isInfix_take
Proof state before:
n m : ℕ
α✝ : Type u_1
l : List α✝
h : n ≤ m
⊢ take n l <:+: take (n + (m - n)) l
Tactic:
simp only [List.take_add, ge_iff_le, isInfix_append_left]
Proof state after:
no goals
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
have ⟨s, t, ih⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <:+: l₃
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
have l₁split := List.take_append_drop (length l₂) l₁
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ l₁ ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
rw [← l₁split] at ih
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
ih : s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t = l₂ ++ l₃
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
apply_fun List.drop (length l₂) at ih
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) (s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t) = drop (length l₂) (l₂ ++ l₃)
⊢ drop (length l₂) l₁ <:+: l₃
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) (s ++ (take (length l₂) l₁ ++ drop (length l₂) l₁) ++ t) = drop (length l₂) (l₂ ++ l₃)
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
simp only [take_append_drop, drop_append_eq_append_drop, ge_iff_le, tsub_le_iff_right,
drop_length, le_refl, tsub_eq_zero_of_le, nil_append, List.drop, List.length_append, Nat.sub_add_eq] at ih
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂) l₁ <:+: l₃
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
suffices drop (length l₂ - length s) l₁ <:+: l₃ by
  apply List.isInfix_trans _ this
  apply List.drop_isInfix_drop
  apply Nat.sub_le
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂ - length s) l₁ <:+: l₃
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
⊢ drop (length l₂ - length s) l₁ <:+: l₃
Tactic:
exists (drop (length l₂) s), (drop (length l₂ - length s - length l₁) t)
Proof state after:
no goals
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ drop (length l₂) l₁ <:+: l₃
Tactic:
apply List.isInfix_trans _ this
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ drop (length l₂) l₁ <:+: drop (length l₂ - length s) l₁
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ drop (length l₂) l₁ <:+: drop (length l₂ - length s) l₁
Tactic:
apply List.drop_isInfix_drop
Proof state after:
case h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ length l₂ ≥ length l₂ - length s
Theorem: List.isInfix_drop_of_isInfix_append
Proof state before:
case h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
s t : List α✝
l₁split : take (length l₂) l₁ ++ drop (length l₂) l₁ = l₁
ih : drop (length l₂) s ++ drop (length l₂ - length s) l₁ ++ drop (length l₂ - length s - length l₁) t = l₃
this : drop (length l₂ - length s) l₁ <:+: l₃
⊢ length l₂ ≥ length l₂ - length s
Tactic:
apply Nat.sub_le
Proof state after:
no goals
Theorem: Nat.min_self_sub_right
Proof state before:
n m : ℕ
⊢ min n (n - m) = n - m
Tactic:
simp only [ge_iff_le, tsub_le_iff_right, le_add_iff_nonneg_right, zero_le, min_eq_right]
Proof state after:
no goals
Theorem: Nat.min_self_sub_left
Proof state before:
n m : ℕ
⊢ min (n - m) n = n - m
Tactic:
rw [min_commutative]
Proof state after:
n m : ℕ
⊢ min n (n - m) = n - m
Theorem: Nat.min_self_sub_left
Proof state before:
n m : ℕ
⊢ min n (n - m) = n - m
Tactic:
apply Nat.min_self_sub_right
Proof state after:
no goals
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have ⟨s,t,ih⟩ := h
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have hl: s.length + l₁.length + t.length = l₂.length + l₃.length := by
  apply_fun @List.length α at ih
  simp only [List.length_append] at ih
  exact ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have l₁split := List.take_append_drop (length l₁ - length l₃) l₁
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
rw [←l₁split] at ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t = l₂ ++ l₃
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
apply_fun List.take (length l₂) at ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) (s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t) =
    take (length l₂) (l₂ ++ l₃)
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) (s ++ (take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁) ++ t) =
    take (length l₂) (l₂ ++ l₃)
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
simp only [List.take_append_eq_append_take, List.take_take, List.length_take, length_drop, length_append,
  take_length, Nat.sub_self, take_zero, append_nil, Nat.min_self_sub_left] at ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ take (length l₁ - length l₃) l₁ <:+: l₂