Theorem: List.isPrefix_take (One.lean)

State before:
α : Type u_1
delim l : List α
⊢ delim <+: take (length delim) l ↔ delim <+: l
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
delim l : List α
⊢ delim <+: take (length delim) l → delim <+: l

case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l

State before:
case mp
α : Type u_1
delim l : List α
⊢ delim <+: take (length delim) l → delim <+: l

case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l
Tactic:
. intro ⟨t, heq⟩
  replace heq := congr_arg (take (length delim)) heq
  simp only [take_left, take_take, min_self] at heq
  rw [heq]
  simp only [take_isPrefix]
State after:
case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l

State before:
case mpr
α : Type u_1
delim l : List α
⊢ delim <+: l → delim <+: take (length delim) l
Tactic:
. intro ⟨t, heq⟩
  subst l
  simp only [take_left, isPrefix_self]
State after:
no goals