internlm/Lean-Github huggingface dataset:
Theorem: List.append_isPrefix_split
Proof state before:
case true
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : decide (length s + length l₁ ≤ n) = true
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
simp only [decide_eq_true_eq] at hle
Proof state after:
case true
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case true
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
left
Proof state after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t)
Tactic:
exists (take (n-length s - length l₁) t)
Proof state after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Tactic:
have hle₁ : length s ≤ n := by  calc
  length s ≤  length s + length l₁ := by simp
         _ ≤  n                     := hle
Proof state after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Tactic:
have hle₂ : length l₁ ≤ (n - length s) := by apply Nat.le_sub_of_add_le; rw [add_comm]; exact hle
Proof state after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = take n (s ++ l₁ ++ t)
Tactic:
rw [List.take_append_eq_append_take, List.take_append_eq_append_take, List.take_all_of_le hle₁, List.take_all_of_le hle₂]
Proof state after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = s ++ l₁ ++ take (n - length (s ++ l₁)) t
Theorem: List.append_isPrefix_split
Proof state before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ s ++ l₁ ++ take (n - length s - length l₁) t = s ++ l₁ ++ take (n - length (s ++ l₁)) t
Tactic:
simp
Proof state after:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ take (n - length s - length l₁) t = take (n - (length s + length l₁)) t
Theorem: List.append_isPrefix_split
Proof state before:
case true.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ take (n - length s - length l₁) t = take (n - (length s + length l₁)) t
Tactic:
congr 1
Proof state after:
case true.h.e_a
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ n - length s - length l₁ = n - (length s + length l₁)
Theorem: List.append_isPrefix_split
Proof state before:
case true.h.e_a
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
hle₂ : length l₁ ≤ n - length s
⊢ n - length s - length l₁ = n - (length s + length l₁)
Tactic:
apply Nat.sub_sub
Proof state after:
no goals
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ length s ≤ n
Tactic:
calc
length s ≤  length s + length l₁ := by simp
_ ≤  n                     := hle
Proof state after:
no goals
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
⊢ length s ≤ length s + length l₁
Tactic:
simp
Proof state after:
no goals
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length l₁ ≤ n - length s
Tactic:
apply Nat.le_sub_of_add_le
Proof state after:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length l₁ + length s ≤ n
Theorem: List.append_isPrefix_split
Proof state before:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length l₁ + length s ≤ n
Tactic:
rw [add_comm]
Proof state after:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length s + length l₁ ≤ n
Theorem: List.append_isPrefix_split
Proof state before:
case h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : length s + length l₁ ≤ n
hle₁ : length s ≤ n
⊢ length s + length l₁ ≤ n
Tactic:
exact hle
Proof state after:
no goals
Theorem: List.append_isPrefix_split
Proof state before:
case false
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : decide (length s + length l₁ ≤ n) = false
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
simp only [decide_eq_false_iff_not, not_le] at hle
Proof state after:
case false
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case false
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
right
Proof state after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Theorem: List.append_isPrefix_split
Proof state before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
rw [List.drop_append_eq_append_drop, List.drop_append_eq_append_drop]
Proof state after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t
Theorem: List.append_isPrefix_split
Proof state before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t
Tactic:
have heq₁: n + 1 - length l₁ - length s = 0 := by
  rw [Nat.sub_sub, Nat.sub_eq_zero_of_le]
  apply Nat.add_one_le_iff.2
  rw [Nat.add_comm]
  apply hle
Proof state after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t
Theorem: List.append_isPrefix_split
Proof state before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+:
    drop (n + 1 - length l₁) s ++ drop (n + 1 - length l₁ - length s) l₁ ++
      drop (n + 1 - length l₁ - length (s ++ l₁)) t
Tactic:
rw [heq₁, drop]
Proof state after:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) s ++ l₁ ++ drop (n + 1 - length l₁ - length (s ++ l₁)) t
Theorem: List.append_isPrefix_split
Proof state before:
case false.h
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
heq₁ : n + 1 - length l₁ - length s = 0
⊢ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) s ++ l₁ ++ drop (n + 1 - length l₁ - length (s ++ l₁)) t
Tactic:
exists (drop (n + 1 - length l₁ - length (s ++ l₁)) t)
Proof state after:
no goals
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n + 1 - length l₁ - length s = 0
Tactic:
rw [Nat.sub_sub, Nat.sub_eq_zero_of_le]
Proof state after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n + 1 ≤ length l₁ + length s
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n + 1 ≤ length l₁ + length s
Tactic:
apply Nat.add_one_le_iff.2
Proof state after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length l₁ + length s
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length l₁ + length s
Tactic:
rw [Nat.add_comm]
Proof state after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length s + length l₁
Theorem: List.append_isPrefix_split
Proof state before:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
hle : n < length s + length l₁
⊢ n < length s + length l₁
Tactic:
apply hle
Proof state after:
no goals
Theorem: List.isInfix_split
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
have ⟨s, hPre⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Theorem: List.isInfix_split
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
cases append_isPrefix_split hPre n with
| inl => left; exists s
| inr => right; exists (drop (n + 1 - length l₁) s)
Proof state after:
no goals
Theorem: List.isInfix_split
Proof state before:
case inl
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : s ++ l₁ <+: take n l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
left
Proof state after:
case inl.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : s ++ l₁ <+: take n l₂
⊢ l₁ <:+: take n l₂
Theorem: List.isInfix_split
Proof state before:
case inl.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : s ++ l₁ <+: take n l₂
⊢ l₁ <:+: take n l₂
Tactic:
exists s
Proof state after:
no goals
Theorem: List.isInfix_split
Proof state before:
case inr
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
⊢ l₁ <:+: take n l₂ ∨ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
right
Proof state after:
case inr.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
⊢ l₁ <:+: drop (n + 1 - length l₁) l₂
Theorem: List.isInfix_split
Proof state before:
case inr.h
α✝ : Type u_1
l₁ l₂ : List α✝
h : l₁ <:+: l₂
n : ℕ
s : List α✝
hPre : ∃ t, s ++ l₁ ++ t = l₂
h✝ : drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
⊢ l₁ <:+: drop (n + 1 - length l₁) l₂
Tactic:
exists (drop (n + 1 - length l₁) s)
Proof state after:
no goals
Theorem: List.isInfix_append_split_left
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
have split := List.isInfix_split h l₂.length
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: take (length l₂) (l₂ ++ l₃) ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Theorem: List.isInfix_append_split_left
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: take (length l₂) (l₂ ++ l₃) ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
simp only [take_left, ge_iff_le]  at split
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: l₂ ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Theorem: List.isInfix_append_split_left
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split : l₁ <:+: l₂ ∨ l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
cases split with
| inl h₁ =>
  left; assumption
| inr h₂ =>
  right
  if hzero: l₁.length = 0 then
    simp [List.length_eq_zero.1 hzero]
  else
    rw [List.drop_append_of_le_length] at h₂
    . rw [lastN]
      convert h₂ using 3
      rw [Nat.sub_sub_eq_add_sub_of_le]
      rw [Nat.succ_le, pos_iff_ne_zero]
      apply hzero
    . simp only [ge_iff_le, tsub_le_iff_right, add_le_add_iff_left]
      rw [Nat.succ_le, pos_iff_ne_zero]
      apply hzero
Proof state after:
no goals
Theorem: List.isInfix_append_split_left
Proof state before:
case inl
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₁ : l₁ <:+: l₂
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
left
Proof state after:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₁ : l₁ <:+: l₂
⊢ l₁ <:+: l₂
Theorem: List.isInfix_append_split_left
Proof state before:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₁ : l₁ <:+: l₂
⊢ l₁ <:+: l₂
Tactic:
assumption
Proof state after:
no goals
Theorem: List.isInfix_append_split_left
Proof state before:
case inr
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ∨ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
right
Proof state after:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Theorem: List.isInfix_append_split_left
Proof state before:
case inr.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
if hzero: l₁.length = 0 then
  simp [List.length_eq_zero.1 hzero]
else
  rw [List.drop_append_of_le_length] at h₂
  . rw [lastN]
    convert h₂ using 3
    rw [Nat.sub_sub_eq_add_sub_of_le]
    rw [Nat.succ_le, pos_iff_ne_zero]
    apply hzero
  . simp only [ge_iff_le, tsub_le_iff_right, add_le_add_iff_left]
    rw [Nat.succ_le, pos_iff_ne_zero]
    apply hzero
Proof state after:
no goals
Theorem: List.isInfix_append_split_left
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : length l₁ = 0
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
simp [List.length_eq_zero.1 hzero]
Proof state after:
no goals
Theorem: List.isInfix_append_split_left
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃
Tactic:
rw [List.drop_append_of_le_length] at h₂
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) l₂ ++ l₃
hzero : ¬length l₁ = 0
⊢ l₁ <:+: lastN (length l₁ - 1) l₂ ++ l₃

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

α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ length l₂ + 1 - length l₁ ≤ length l₂
Tactic:
. rw [lastN]
  convert h₂ using 3
  rw [Nat.sub_sub_eq_add_sub_of_le]
  rw [Nat.succ_le, pos_iff_ne_zero]
  apply hzero
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ length l₂ + 1 - length l₁ ≤ length l₂
Theorem: List.isInfix_append_split_left
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
h₂ : l₁ <:+: drop (length l₂ + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ length l₂ + 1 - length l₁ ≤ length l₂
Tactic:
. simp only [ge_iff_le, tsub_le_iff_right, add_le_add_iff_left]
  rw [Nat.succ_le, pos_iff_ne_zero]
  apply hzero
Proof state after:
no goals
Theorem: List.isInfix_append_split_right
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
have split := List.isInfix_split h (l₂.length + (l₁.length -1))
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Theorem: List.isInfix_append_split_right
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
if hzero: l₁.length = 0 then
    simp only [List.length_eq_zero.1 hzero, length_nil, ge_iff_le, tsub_eq_zero_of_le, append_nil, nil_isInfix, or_self]
else
  cases split with
  | inl h₁ =>
    left
    rw [List.take_append] at h₁
    exact h₁
  | inr h₂ =>
    right
    rw [add_assoc, Nat.sub_add_cancel, Nat.add_sub_cancel, ←Nat.add_zero l₂.length, List.drop_append, List.drop] at h₂
    . exact h₂
    . rw [Nat.succ_le_iff, Nat.pos_iff_ne_zero]
      exact hzero
Proof state after:
no goals
Theorem: List.isInfix_append_split_right
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
hzero : length l₁ = 0
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
simp only [List.length_eq_zero.1 hzero, length_nil, ge_iff_le, tsub_eq_zero_of_le, append_nil, nil_isInfix, or_self]
Proof state after:
no goals
Theorem: List.isInfix_append_split_right
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
split :
  l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃) ∨
    l₁ <:+: drop (length l₂ + (length l₁ - 1) + 1 - length l₁) (l₂ ++ l₃)
hzero : ¬length l₁ = 0
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
cases split with
| inl h₁ =>
  left
  rw [List.take_append] at h₁
  exact h₁
| inr h₂ =>
  right
  rw [add_assoc, Nat.sub_add_cancel, Nat.add_sub_cancel, ←Nat.add_zero l₂.length, List.drop_append, List.drop] at h₂
  . exact h₂
  . rw [Nat.succ_le_iff, Nat.pos_iff_ne_zero]
    exact hzero
Proof state after:
no goals
Theorem: List.isInfix_append_split_right
Proof state before:
case inl
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
left
Proof state after:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
Theorem: List.isInfix_append_split_right
Proof state before:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: take (length l₂ + (length l₁ - 1)) (l₂ ++ l₃)
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
Tactic:
rw [List.take_append] at h₁
Proof state after:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
Theorem: List.isInfix_append_split_right
Proof state before:
case inl.h
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂ ++ l₃
hzero : ¬length l₁ = 0
h₁ : l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
⊢ l₁ <:+: l₂ ++ take (length l₁ - 1) l₃
Tactic:
exact h₁
Proof state after:
no goals
Theorem: List.isInfix_append_split_right
Proof state before:
case inr
α✝ : 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₂ ++ take (length l₁ - 1) l₃ ∨ l₁ <:+: l₃
Tactic:
right
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₃)
⊢ l₁ <:+: l₃