internlm/Lean-Github huggingface dataset:
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
h : isInfixOf delim (head :: tail) = true
⊢ delim <:+: head :: tail
Tactic:
unfold isInfixOf at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
h :
  (match delim, head :: tail with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
⊢ delim <:+: head :: tail
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
h :
  (match delim, head :: tail with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
⊢ delim <:+: head :: tail
Tactic:
simp at h
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
h : isPrefixOf delim (head :: tail) = true ∨ isInfixOf delim tail = true
⊢ delim <:+: head :: tail
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
h : isPrefixOf delim (head :: tail) = true ∨ isInfixOf delim tail = true
⊢ delim <:+: head :: tail
Tactic:
cases h with
| inl heq =>
  simp only [List.isPrefixOf_ext] at heq
  simp only [heq, List.isInfix_of_isPrefix]
| inr heq =>
  have h₂:= ih heq
  apply List.isInfix_cons h₂
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
case inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
heq : isPrefixOf delim (head :: tail) = true
⊢ delim <:+: head :: tail
Tactic:
simp only [List.isPrefixOf_ext] at heq
Proof state after:
case inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
heq : delim <+: head :: tail
⊢ delim <:+: head :: tail
Theorem: List.isInfixOf_ext
Proof state before:
case inl
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
heq : delim <+: head :: tail
⊢ delim <:+: head :: tail
Tactic:
simp only [heq, List.isInfix_of_isPrefix]
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
case inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
heq : isInfixOf delim tail = true
⊢ delim <:+: head :: tail
Tactic:
have h₂:= ih heq
Proof state after:
case inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
heq : isInfixOf delim tail = true
h₂ : delim <:+: tail
⊢ delim <:+: head :: tail
Theorem: List.isInfixOf_ext
Proof state before:
case inr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
head : α
tail : List α
ih : isInfixOf delim tail = true → delim <:+: tail
heq : isInfixOf delim tail = true
h₂ : delim <:+: tail
⊢ delim <:+: head :: tail
Tactic:
apply List.isInfix_cons h₂
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
⊢ isInfixOf delim ([] ++ delim ++ t) = true
Tactic:
unfold isInfixOf
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
⊢ (match delim, [] ++ delim ++ t with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
⊢ (match delim, [] ++ delim ++ t with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
Tactic:
split
Proof state after:
case h_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝¹ x✝ : List α
heq✝ : [] ++ [] ++ t = []
⊢ true = true

case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
heq✝ : [] ++ x✝³ ++ t = []
⊢ false = true

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] ++ x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝¹ x✝ : List α
heq✝ : [] ++ [] ++ t = []
⊢ true = true
Tactic:
case h_1 => simp only
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
hne : x✝² = [] → False
heq : [] ++ x✝² ++ t = []
⊢ false = true
Tactic:
case h_2 hne heq => simp_all only [nil_append, append_eq_nil, forall_true_left]
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : [] ++ x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
Tactic:
case h_3 heq => 
  simp at heq
  rw [← heq]
  simp only [Bool.or_eq_true, List.isPrefixOf_ext]
  left
  exists t
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝¹ x✝ : List α
heq✝ : [] ++ [] ++ t = []
⊢ true = true
Tactic:
simp only
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
hne : x✝² = [] → False
heq : [] ++ x✝² ++ t = []
⊢ false = true
Tactic:
simp_all only [nil_append, append_eq_nil, forall_true_left]
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : [] ++ x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
Tactic:
simp at heq
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
Tactic:
rw [← heq]
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (x✝² ++ t) || isInfixOf x✝² as✝) = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (x✝² ++ t) || isInfixOf x✝² as✝) = true
Tactic:
simp only [Bool.or_eq_true, List.isPrefixOf_ext]
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ x✝² <+: x✝² ++ t ∨ isInfixOf x✝² as✝ = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ x✝² <+: x✝² ++ t ∨ isInfixOf x✝² as✝ = true
Tactic:
left
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ x✝² <+: x✝² ++ t
Theorem: List.isInfixOf_ext
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : x✝² ++ t = a✝ :: as✝
⊢ x✝² <+: x✝² ++ t
Tactic:
exists t
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
head : α
tail : List α
ih : isInfixOf delim (tail ++ delim ++ t) = true
⊢ isInfixOf delim (head :: tail ++ delim ++ t) = true
Tactic:
unfold isInfixOf
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
head : α
tail : List α
ih : isInfixOf delim (tail ++ delim ++ t) = true
⊢ (match delim, head :: tail ++ delim ++ t with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
head : α
tail : List α
ih : isInfixOf delim (tail ++ delim ++ t) = true
⊢ (match delim, head :: tail ++ delim ++ t with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
Tactic:
split
Proof state after:
case h_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝¹ x✝ : List α
ih : isInfixOf [] (tail ++ [] ++ t) = true
heq✝ : head :: tail ++ [] ++ t = []
⊢ true = true

case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
ih : isInfixOf x✝³ (tail ++ x✝³ ++ t) = true
heq✝ : head :: tail ++ x✝³ ++ t = []
⊢ false = true

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq✝ : head :: tail ++ x✝² ++ t = a✝ :: as✝
⊢ (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝¹ x✝ : List α
ih : isInfixOf [] (tail ++ [] ++ t) = true
heq : head :: tail ++ [] ++ t = []
⊢ true = true
Tactic:
case h_1 heq=>
  simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hne : x✝² = [] → False
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head :: tail ++ x✝² ++ t = []
⊢ false = true
Tactic:
case h_2 hne heq =>
  simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head :: tail ++ x✝² ++ t = hd :: tl
⊢ (isPrefixOf x✝² (hd :: tl) || isInfixOf x✝² tl) = true
Tactic:
case h_3 hd tl heq =>
  simp at heq
  have ⟨h₁, h₂⟩ := heq
  simp only [Bool.or_eq_true]
  right
  rw [ ← h₂]
  rw [append_assoc] at ih
  apply ih
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝¹ x✝ : List α
ih : isInfixOf [] (tail ++ [] ++ t) = true
heq : head :: tail ++ [] ++ t = []
⊢ true = true
Tactic:
simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hne : x✝² = [] → False
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head :: tail ++ x✝² ++ t = []
⊢ false = true
Tactic:
simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
Proof state after:
no goals
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head :: tail ++ x✝² ++ t = hd :: tl
⊢ (isPrefixOf x✝² (hd :: tl) || isInfixOf x✝² tl) = true
Tactic:
simp at heq
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
⊢ (isPrefixOf x✝² (hd :: tl) || isInfixOf x✝² tl) = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
⊢ (isPrefixOf x✝² (hd :: tl) || isInfixOf x✝² tl) = true
Tactic:
have ⟨h₁, h₂⟩ := heq
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ (isPrefixOf x✝² (hd :: tl) || isInfixOf x✝² tl) = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ (isPrefixOf x✝² (hd :: tl) || isInfixOf x✝² tl) = true
Tactic:
simp only [Bool.or_eq_true]
Proof state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isPrefixOf x✝² (hd :: tl) = true ∨ isInfixOf x✝² tl = true
Theorem: List.isInfixOf_ext
Proof state before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isPrefixOf x✝² (hd :: tl) = true ∨ isInfixOf x✝² tl = true
Tactic:
right
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isInfixOf x✝² tl = true
Theorem: List.isInfixOf_ext
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isInfixOf x✝² tl = true
Tactic:
rw [ ← h₂]
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isInfixOf x✝² (tail ++ (x✝² ++ t)) = true
Theorem: List.isInfixOf_ext
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ x✝² ++ t) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isInfixOf x✝² (tail ++ (x✝² ++ t)) = true
Tactic:
rw [append_assoc] at ih
Proof state after:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ (x✝² ++ t)) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isInfixOf x✝² (tail ++ (x✝² ++ t)) = true
Theorem: List.isInfixOf_ext
Proof state before:
case h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
head : α
tail x✝² x✝¹ x✝ : List α
hd : α
tl : List α
ih : isInfixOf x✝² (tail ++ (x✝² ++ t)) = true
heq : head = hd ∧ tail ++ (x✝² ++ t) = tl
h₁ : head = hd
h₂ : tail ++ (x✝² ++ t) = tl
⊢ isInfixOf x✝² (tail ++ (x✝² ++ t)) = true
Tactic:
apply ih
Proof state after:
no goals
Theorem: List.isPrefix_self_append
Proof state before:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <+: l₁ ++ l₂
Tactic:
exists l₂
Proof state after:
no goals
Theorem: List.isPostfix_append_of_isPostfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
⊢ l₁ <:+ l₃ ++ l₂
Tactic:
have ⟨s, heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ l₂
Theorem: List.isPostfix_append_of_isPostfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ l₂
Tactic:
rw [← heq]
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ (s ++ l₁)
Theorem: List.isPostfix_append_of_isPostfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₁ <:+ l₃ ++ (s ++ l₁)
Tactic:
exists l₃ ++ s
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₃ ++ s ++ l₁ = l₃ ++ (s ++ l₁)
Theorem: List.isPostfix_append_of_isPostfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+ l₂
s : List α✝
heq : s ++ l₁ = l₂
⊢ l₃ ++ s ++ l₁ = l₃ ++ (s ++ l₁)
Tactic:
rw [append_assoc]
Proof state after:
no goals
Theorem: List.isInfix_append_left_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
⊢ l₁ <:+: l₃ ++ l₂
Tactic:
have ⟨s, t, heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₃ ++ l₂
Theorem: List.isInfix_append_left_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₃ ++ l₂
Tactic:
rw [← heq]
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₃ ++ (s ++ l₁ ++ t)
Theorem: List.isInfix_append_left_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₃ ++ (s ++ l₁ ++ t)
Tactic:
exists l₃ ++ s, t
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₃ ++ s ++ l₁ ++ t = l₃ ++ (s ++ l₁ ++ t)
Theorem: List.isInfix_append_left_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₃ ++ s ++ l₁ ++ t = l₃ ++ (s ++ l₁ ++ t)
Tactic:
simp only [append_assoc]
Proof state after:
no goals
Theorem: List.isInfix_append_right_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
⊢ l₁ <:+: l₂ ++ l₃
Tactic:
have ⟨s, t, heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₂ ++ l₃
Theorem: List.isInfix_append_right_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: l₂ ++ l₃
Tactic:
rw [← heq]
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: s ++ l₁ ++ t ++ l₃
Theorem: List.isInfix_append_right_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ l₁ <:+: s ++ l₁ ++ t ++ l₃
Tactic:
exists s, t ++ l₃
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ ++ (t ++ l₃) = s ++ l₁ ++ t ++ l₃
Theorem: List.isInfix_append_right_of_isInfix
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <:+: l₂
s t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ ++ (t ++ l₃) = s ++ l₁ ++ t ++ l₃
Tactic:
simp only [append_assoc]
Proof state after:
no goals
Theorem: List.isPrefix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂ ∧ drop (length l₂) l₁ <+: l₃
Tactic:
have ⟨t, heq⟩ := h
Proof state after:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂ ∧ drop (length l₂) l₁ <+: l₃
Theorem: List.isPrefix_append
Proof state before:
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂ ∧ drop (length l₂) l₁ <+: l₃
Tactic:
apply And.intro
Proof state after:
case left
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂

case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃
Theorem: List.isPrefix_append
Proof state before:
case left
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ take (length l₂) l₁ <+: l₂

case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃
Tactic:
. apply_fun take (length l₂) at heq
  simp only [take_append_eq_append_take, tsub_le_iff_right, ge_iff_le, take_length, Nat.sub_self, zero_le,
    nonpos_iff_eq_zero, le_refl, tsub_eq_zero_of_le, append_nil, take] at heq
  conv => right; rw [← heq]
  apply isPrefix_self_append
Proof state after:
case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃
Theorem: List.isPrefix_append
Proof state before:
case right
α✝ : Type u_1
l₁ l₂ l₃ : List α✝
h : l₁ <+: l₂ ++ l₃
t : List α✝
heq : l₁ ++ t = l₂ ++ l₃
⊢ drop (length l₂) l₁ <+: l₃
Tactic:
. apply_fun drop (length l₂) at heq
  simp only [drop_append_eq_append_drop, tsub_le_iff_right, ge_iff_le, drop_length, Nat.sub_self, zero_le,
    nonpos_iff_eq_zero, le_refl, tsub_eq_zero_of_le, nil_append, drop] at heq
  conv => right; rw [← heq]
  apply isPrefix_self_append
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 : ℕ
⊢ s ++ l₁ <+: take n l₂ ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
Tactic:
have ⟨t,heq⟩ := h
Proof state after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ <+: take n l₂ ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) 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₂
⊢ s ++ l₁ <+: take n l₂ ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) l₂
Tactic:
rw [← heq]
Proof state after:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = 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:
α✝ : Type u_1
s l₁ l₂ : List α✝
h : s ++ l₁ <+: l₂
n : ℕ
t : List α✝
heq : s ++ l₁ ++ t = l₂
⊢ s ++ l₁ <+: take n (s ++ l₁ ++ t) ∨ drop (n + 1 - length l₁) s ++ l₁ <+: drop (n + 1 - length l₁) (s ++ l₁ ++ t)
Tactic:
cases hle: decide (length s + length l₁ ≤ n) with
| true =>
  simp only [decide_eq_true_eq] at hle
  left
  exists (take (n-length s - length l₁) t)
  have hle₁ : length s ≤ n := by  calc
    length s ≤  length s + length l₁ := by simp
           _ ≤  n                     := hle
  have hle₂ : length l₁ ≤ (n - length s) := by apply Nat.le_sub_of_add_le; rw [add_comm]; exact hle
  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₂]
  simp
  congr 1
  apply Nat.sub_sub
| false =>
  simp only [decide_eq_false_iff_not, not_le] at hle
  right
  rw [List.drop_append_eq_append_drop, List.drop_append_eq_append_drop]
  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
  rw [heq₁, drop]
  exists (drop (n + 1 - length l₁ - length (s ++ l₁)) t)
Proof state after:
no goals