internlm/Lean-Github huggingface dataset:
Theorem: List.isInfix_append_split_right
Proof state before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₃
Tactic:
rw [add_assoc, Nat.sub_add_cancel, Nat.add_sub_cancel, ←Nat.add_zero l₂.length, List.drop_append, List.drop] at h₂
Proof state after:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: l₃
⊢ l₁ <:+: l₃

case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁
Theorem: List.isInfix_append_split_right
Proof state before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: l₃
⊢ l₁ <:+: l₃

case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁
Tactic:
. exact h₂
Proof state after:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁
Theorem: List.isInfix_append_split_right
Proof state before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₂ : l₁ <:+: drop (length l₂ + (length l₁ - 1 + 1) - length l₁) (l₂ ++ l₃)
⊢ 1 ≤ length l₁
Tactic:
. rw [Nat.succ_le_iff, Nat.pos_iff_ne_zero]
  exact hzero
Proof state after:
no goals
Theorem: List.isInfix_of_isInfix_take
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
⊢ l₁ <:+: l₂
Tactic:
rw [← List.take_append_drop n l₂]
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Theorem: List.isInfix_of_isInfix_take
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Tactic:
have ⟨s,t,heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
s t : List α✝
heq : s ++ l₁ ++ t = take n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Theorem: List.isInfix_of_isInfix_take
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
s t : List α✝
heq : s ++ l₁ ++ t = take n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Tactic:
exists s, t ++ drop n l₂
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
s t : List α✝
heq : s ++ l₁ ++ t = take n l₂
⊢ s ++ l₁ ++ (t ++ drop n l₂) = take n l₂ ++ drop n l₂
Theorem: List.isInfix_of_isInfix_take
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: take n l₂
s t : List α✝
heq : s ++ l₁ ++ t = take n l₂
⊢ s ++ l₁ ++ (t ++ drop n l₂) = take n l₂ ++ drop n l₂
Tactic:
simp only [append_assoc, ← heq]
Proof state after:
no goals
Theorem: List.isInfix_of_isInfix_drop
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
⊢ l₁ <:+: l₂
Tactic:
rw [← List.take_append_drop n l₂]
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Theorem: List.isInfix_of_isInfix_drop
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Tactic:
have ⟨s,t,heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
s t : List α✝
heq : s ++ l₁ ++ t = drop n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Theorem: List.isInfix_of_isInfix_drop
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
s t : List α✝
heq : s ++ l₁ ++ t = drop n l₂
⊢ l₁ <:+: take n l₂ ++ drop n l₂
Tactic:
exists take n l₂ ++ s, t
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
s t : List α✝
heq : s ++ l₁ ++ t = drop n l₂
⊢ take n l₂ ++ s ++ l₁ ++ t = take n l₂ ++ drop n l₂
Theorem: List.isInfix_of_isInfix_drop
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop n l₂
s t : List α✝
heq : s ++ l₁ ++ t = drop n l₂
⊢ take n l₂ ++ s ++ l₁ ++ t = take n l₂ ++ drop n l₂
Tactic:
simp only [append_assoc, ← heq]
Proof state after:
no goals
Theorem: List.isInfix_of_isInfix_lastN
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: lastN n l₂
⊢ l₁ <:+: l₂
Tactic:
rw [lastN] at h
Proof state after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop (length l₂ - n) l₂
⊢ l₁ <:+: l₂
Theorem: List.isInfix_of_isInfix_lastN
Proof state before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop (length l₂ - n) l₂
⊢ l₁ <:+: l₂
Tactic:
apply List.isInfix_of_isInfix_drop h
Proof state after:
no goals
Theorem: List.isPrefix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
⊢ l₁ <+: l₃
Tactic:
have ⟨t₁, heq₁⟩ := h₁
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
t₁ : List α✝
heq₁ : l₁ ++ t₁ = l₂
⊢ l₁ <+: l₃
Theorem: List.isPrefix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
t₁ : List α✝
heq₁ : l₁ ++ t₁ = l₂
⊢ l₁ <+: l₃
Tactic:
have ⟨t₂, heq₂⟩ := h₂
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
t₁ : List α✝
heq₁ : l₁ ++ t₁ = l₂
t₂ : List α✝
heq₂ : l₂ ++ t₂ = l₃
⊢ l₁ <+: l₃
Theorem: List.isPrefix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
t₁ : List α✝
heq₁ : l₁ ++ t₁ = l₂
t₂ : List α✝
heq₂ : l₂ ++ t₂ = l₃
⊢ l₁ <+: l₃
Tactic:
rw [← heq₂, ←heq₁, append_assoc]
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
t₁ : List α✝
heq₁ : l₁ ++ t₁ = l₂
t₂ : List α✝
heq₂ : l₂ ++ t₂ = l₃
⊢ l₁ <+: l₁ ++ (t₁ ++ t₂)
Theorem: List.isPrefix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <+: l₂
h₂ : l₂ <+: l₃
t₁ : List α✝
heq₁ : l₁ ++ t₁ = l₂
t₂ : List α✝
heq₂ : l₂ ++ t₂ = l₃
⊢ l₁ <+: l₁ ++ (t₁ ++ t₂)
Tactic:
exists (t₁ ++ t₂)
Proof state after:
no goals
Theorem: List.isInfix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
⊢ l₁ <:+: l₃
Tactic:
have ⟨s₁, t₁, heq₁⟩ := h₁
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
⊢ l₁ <:+: l₃
Theorem: List.isInfix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
⊢ l₁ <:+: l₃
Tactic:
have ⟨s₂, t₂, heq₂⟩ := h₂
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
s₂ t₂ : List α✝
heq₂ : s₂ ++ l₂ ++ t₂ = l₃
⊢ l₁ <:+: l₃
Theorem: List.isInfix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
s₂ t₂ : List α✝
heq₂ : s₂ ++ l₂ ++ t₂ = l₃
⊢ l₁ <:+: l₃
Tactic:
rw [← heq₂, ←heq₁, append_assoc]
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
s₂ t₂ : List α✝
heq₂ : s₂ ++ l₂ ++ t₂ = l₃
⊢ l₁ <:+: s₂ ++ (s₁ ++ l₁ ++ t₁ ++ t₂)
Theorem: List.isInfix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
s₂ t₂ : List α✝
heq₂ : s₂ ++ l₂ ++ t₂ = l₃
⊢ l₁ <:+: s₂ ++ (s₁ ++ l₁ ++ t₁ ++ t₂)
Tactic:
exists (s₂ ++ s₁), (t₁ ++ t₂)
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
s₂ t₂ : List α✝
heq₂ : s₂ ++ l₂ ++ t₂ = l₃
⊢ s₂ ++ s₁ ++ l₁ ++ (t₁ ++ t₂) = s₂ ++ (s₁ ++ l₁ ++ t₁ ++ t₂)
Theorem: List.isInfix_trans
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h₁ : l₁ <:+: l₂
h₂ : l₂ <:+: l₃
s₁ t₁ : List α✝
heq₁ : s₁ ++ l₁ ++ t₁ = l₂
s₂ t₂ : List α✝
heq₂ : s₂ ++ l₂ ++ t₂ = l₃
⊢ s₂ ++ s₁ ++ l₁ ++ (t₁ ++ t₂) = s₂ ++ (s₁ ++ l₁ ++ t₁ ++ t₂)
Tactic:
simp only [append_assoc]
Proof state after:
no goals
Theorem: List.isInfix_first_match
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
have ⟨s, t, heq⟩ := h
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
cases hinf: List.isInfixOf l₁ (s ++ dropLast l₁) with
| true => 
  simp [List.isInfixOf_ext] at hinf
  have _ : length s + (length l₁ - 1) < length l₂ := by 
    rw[← heq]
    simp only [length_append, length_dropLast, tsub_le_iff_right, ge_iff_le, append_assoc, add_lt_add_iff_left]
    apply Nat.lt_add_right
    apply Nat.sub_lt
    . apply Nat.pos_of_ne_zero
      simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, hne, not_false_iff]
    . simp only
  
  have  ⟨s₁, ih⟩  := List.isInfix_first_match _ _ hinf hne
  exists s₁
  apply And.intro
  . rw [← heq]
    apply isPrefix_trans ih.left
    exists (l₁.lastN 1) ++ t
    rw [dropLast_eq_take, lastN, Nat.pred_eq_sub_one]
    simp only [tsub_le_iff_right, ge_iff_le, append_assoc, append_cancel_left_eq]
    rw [← append_assoc, List.take_append_drop (length l₁ - 1) l₁]
    
  . exact ih.right
| false =>
  exists s
  apply And.intro
  . exists t
  . simp only [←isInfixOf_ext, hinf, not_false_iff]
Proof state after:
no goals
Theorem: List.isInfix_first_match
Proof state before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = true
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
simp [List.isInfixOf_ext] at hinf
Proof state after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
have _ : length s + (length l₁ - 1) < length l₂ := by 
  rw[← heq]
  simp only [length_append, length_dropLast, tsub_le_iff_right, ge_iff_le, append_assoc, add_lt_add_iff_left]
  apply Nat.lt_add_right
  apply Nat.sub_lt
  . apply Nat.pos_of_ne_zero
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, hne, not_false_iff]
  . simp only
Proof state after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
have  ⟨s₁, ih⟩  := List.isInfix_first_match _ _ hinf hne
Proof state after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
exists s₁
Proof state after:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case true
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
Tactic:
apply And.intro
Proof state after:
case true.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂

case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case true.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ s₁ ++ l₁ <+: l₂

case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁
Tactic:
. rw [← heq]
  apply isPrefix_trans ih.left
  exists (l₁.lastN 1) ++ t
  rw [dropLast_eq_take, lastN, Nat.pred_eq_sub_one]
  simp only [tsub_le_iff_right, ge_iff_le, append_assoc, append_cancel_left_eq]
  rw [← append_assoc, List.take_append_drop (length l₁ - 1) l₁]
Proof state after:
case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case true.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
x✝ : length s + (length l₁ - 1) < length l₂
s₁ : List α
ih : s₁ ++ l₁ <+: s ++ dropLast l₁ ∧ ¬l₁ <:+: s₁ ++ dropLast l₁
⊢ ¬l₁ <:+: s₁ ++ dropLast l₁
Tactic:
. exact ih.right
Proof state after:
no goals
Theorem: List.isInfix_first_match
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length s + (length l₁ - 1) < length l₂
Tactic:
rw[← heq]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length s + (length l₁ - 1) < length (s ++ l₁ ++ t)
Theorem: List.isInfix_first_match
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length s + (length l₁ - 1) < length (s ++ l₁ ++ t)
Tactic:
simp only [length_append, length_dropLast, tsub_le_iff_right, ge_iff_le, append_assoc, add_lt_add_iff_left]
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁ + length t
Theorem: List.isInfix_first_match
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁ + length t
Tactic:
apply Nat.lt_add_right
Proof state after:
case h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁
Theorem: List.isInfix_first_match
Proof state before:
case h
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ length l₁ - 1 < length l₁
Tactic:
apply Nat.sub_lt
Proof state after:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < length l₁

case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1
Theorem: List.isInfix_first_match
Proof state before:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < length l₁

case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1
Tactic:
. apply Nat.pos_of_ne_zero
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, hne, not_false_iff]
Proof state after:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1
Theorem: List.isInfix_first_match
Proof state before:
case h.a
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : l₁ <:+: s ++ dropLast l₁
⊢ 0 < 1
Tactic:
. simp only
Proof state after:
no goals
Theorem: List.isInfix_first_match
Proof state before:
case false
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ∃ s, s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
exists s
Proof state after:
case false
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case false
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂ ∧ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
apply And.intro
Proof state after:
case false.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂

case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case false.left
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ s ++ l₁ <+: l₂

case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
. exists t
Proof state after:
case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁
Theorem: List.isInfix_first_match
Proof state before:
case false.right
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
h : l₁ <:+: l₂
hne : l₁ ≠ []
s t : List α
heq : s ++ l₁ ++ t = l₂
hinf : isInfixOf l₁ (s ++ dropLast l₁) = false
⊢ ¬l₁ <:+: s ++ dropLast l₁
Tactic:
. simp only [←isInfixOf_ext, hinf, not_false_iff]
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 α
l : List α
⊢ splitOnListAux delim l acc r h ≠ #[]
Tactic:
unfold splitOnListAux
Proof state after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
l : List α
⊢ (match _h₀ : l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        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 α
l : List α
⊢ (match _h₀ : l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Tactic:
cases l with
| nil => simp only; intro contr; rw [Array.ext_iff] at contr; simp only [Array.push_data, Array.data_toArray, append_eq_nil, and_false] at contr
| cons head tail =>
  simp only
  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:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
⊢ (match _h₀ : [] with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest [] delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf []);
        splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Tactic:
simp only
Proof state after:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
⊢ Array.push r acc ≠ #[]
Theorem: List.splitOnListAux_ne_nil
Proof state before:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
⊢ Array.push r acc ≠ #[]
Tactic:
intro contr
Proof state after:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : Array.push r acc = #[]
⊢ False
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 = #[]
⊢ False
Tactic:
rw [Array.ext_iff] at contr
Proof state after:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : (Array.push r acc).data = #[].data
⊢ False