Theorem: List.isInfixOf_ext (One.lean)

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isInfixOf delim l = true ↔ delim <:+: l
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isInfixOf delim l = true → delim <:+: l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true

State before:
case mp
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ isInfixOf delim l = true → delim <:+: l

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true
Tactic:
. intro h
  induction l
  case nil => 
    unfold isInfixOf at h
    split at h
    . simp only [nil_isInfix]
    . simp only at h
    . next heq => simp only at heq
  case cons head tail ih =>
    unfold isInfixOf at h
    simp at h
    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₂
State after:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true

State before:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <:+: l → isInfixOf delim l = true
Tactic:
. intro h
  have ⟨s,t, heq⟩ := h
  subst heq
  clear h
  induction s
  case nil =>
    unfold isInfixOf
    split
    case h_1 => simp only
    case h_2 hne heq => simp_all only [nil_append, append_eq_nil, forall_true_left]
    case h_3 heq => 
      simp at heq
      rw [← heq]
      simp only [Bool.or_eq_true, List.isPrefixOf_ext]
      left
      exists t
  case cons head tail ih =>
    unfold isInfixOf
    split
    case h_1 heq=>
      simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
    case h_2 hne heq =>
      simp only [append_assoc, cons_append, append_eq_nil, and_false] at heq
    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
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h : isInfixOf delim [] = true
⊢ delim <:+: []
Tactic:
unfold isInfixOf at h
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
⊢ delim <:+: []

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], [] => true
    | x, [] => false
    | delim, a :: as => isPrefixOf delim (a :: as) || isInfixOf delim as) =
    true
⊢ delim <:+: []
Tactic:
split at h
State after:
case h_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝¹ x✝ : List α
heq✝ : [] = []
h : true = true
⊢ [] <:+: []

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

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []

State before:
case h_1
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝¹ x✝ : List α
heq✝ : [] = []
h : true = true
⊢ [] <:+: []

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

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
. simp only [nil_isInfix]
State after:
case h_2
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝³ x✝² x✝¹ : List α
x✝ : x✝³ = [] → False
heq✝ : [] = []
h : false = true
⊢ x✝³ <:+: []

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []

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

case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
. simp only at h
State after:
case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []

State before:
case h_3
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq✝ : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
. next heq => simp only at heq
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x✝² x✝¹ x✝ : List α
a✝ : α
as✝ : List α
heq : [] = a✝ :: as✝
h : (isPrefixOf x✝² (a✝ :: as✝) || isInfixOf x✝² as✝) = true
⊢ x✝² <:+: []
Tactic:
simp only at heq
State after:
no goals

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
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

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
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

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₂
State after:
no goals

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
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

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]
State after:
no goals

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
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

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₂
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim t : List α
⊢ isInfixOf delim ([] ++ delim ++ t) = true
Tactic:
unfold isInfixOf
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

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
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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝¹ x✝ : List α
heq✝ : [] ++ [] ++ t = []
⊢ true = true
Tactic:
case h_1 => simp only
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t x✝¹ x✝ : List α
heq✝ : [] ++ [] ++ t = []
⊢ true = true
Tactic:
simp only
State after:
no goals

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]
State after:
no goals

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
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

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]
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

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]
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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]
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

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
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

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₂]
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

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
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

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
State after:
no goals