Theorem: List.isPrefixOf_ext (One.lean)

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

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

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

case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true
Tactic:
. intro h
  induction l  generalizing delim
  case nil =>
    unfold isPrefixOf at h
    cases delim <;> simp_all only [isPrefix_self]
  case cons head tail ih =>
    unfold isPrefixOf at h
    cases delim
    case nil => simp only [append_nil, nil_isPrefix]
    case cons dhead dtail =>
      simp at h
      have ⟨h₂,h₃⟩ := h
      have ⟨s, heq⟩  := ih dtail h₃
      exists s
      simp only [h₂, cons_append, heq]
State after:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true

State before:
case mpr
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim l : List α
⊢ delim <+: l → isPrefixOf delim l = true
Tactic:
. intro h
  have ⟨s, heq⟩ := h
  rw [← heq]
  clear heq h
  induction delim generalizing l
  case nil =>
    unfold isPrefixOf
    simp only
  case cons head tail ih =>
    unfold isPrefixOf
    simp
    apply ih l
State after:
no goals

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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
delim : List α
h :
  (match delim, [] with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ delim <+: []
Tactic:
cases delim <;> simp_all only [isPrefix_self]
State after:
no goals

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

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
delim : List α
h :
  (match delim, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ delim <+: head :: tail
Tactic:
cases delim
State after:
case nil
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
h :
  (match [], head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ [] <+: head :: tail

case cons
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
head✝ : α
tail✝ : List α
h :
  (match head✝ :: tail✝, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ head✝ :: tail✝ <+: head :: tail

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
h :
  (match [], head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ [] <+: head :: tail
Tactic:
case nil => simp only [append_nil, nil_isPrefix]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h :
  (match dhead :: dtail, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ dhead :: dtail <+: head :: tail
Tactic:
case cons dhead dtail =>
  simp at h
  have ⟨h₂,h₃⟩ := h
  have ⟨s, heq⟩  := ih dtail h₃
  exists s
  simp only [h₂, cons_append, heq]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
h :
  (match [], head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ [] <+: head :: tail
Tactic:
simp only [append_nil, nil_isPrefix]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h :
  (match dhead :: dtail, head :: tail with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
⊢ dhead :: dtail <+: head :: tail
Tactic:
simp at h
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail
Tactic:
have ⟨h₂,h₃⟩ := h
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
⊢ dhead :: dtail <+: head :: tail
Tactic:
have ⟨s, heq⟩  := ih dtail h₃
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail <+: head :: tail

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail <+: head :: tail
Tactic:
exists s
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail ++ s = head :: tail

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
head : α
tail : List α
ih : ∀ (delim : List α), isPrefixOf delim tail = true → delim <+: tail
dhead : α
dtail : List α
h : dhead = head ∧ isPrefixOf dtail tail = true
h₂ : dhead = head
h₃ : isPrefixOf dtail tail = true
s : List α
heq : dtail ++ s = tail
⊢ dhead :: dtail ++ s = head :: tail
Tactic:
simp only [h₂, cons_append, heq]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s l : List α
⊢ isPrefixOf [] ([] ++ s) = true
Tactic:
unfold isPrefixOf
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s l : List α
⊢ (match [], [] ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s l : List α
⊢ (match [], [] ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
Tactic:
simp only
State after:
no goals

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ isPrefixOf (head :: tail) (head :: tail ++ s) = true
Tactic:
unfold isPrefixOf
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ (match head :: tail, head :: tail ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ (match head :: tail, head :: tail ++ s with
    | [], x => true
    | x, [] => false
    | a :: as, b :: bs => a == b && isPrefixOf as bs) =
    true
Tactic:
simp
State after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ isPrefixOf tail (tail ++ s) = true

State before:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
s : List α
head : α
tail : List α
ih : List α → isPrefixOf tail (tail ++ s) = true
l : List α
⊢ isPrefixOf tail (tail ++ s) = true
Tactic:
apply ih l
State after:
no goals