Theorem: List.isInfix_cons (One.lean)

State before:
α : Type u_1
head : α
l tail : List α
h : l <:+: tail
⊢ l <:+: head :: tail
Tactic:
unfold List.isInfix at *
State after:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
⊢ ∃ s t, s ++ l ++ t = head :: tail

State before:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
⊢ ∃ s t, s ++ l ++ t = head :: tail
Tactic:
match h with
| ⟨s,  t, P⟩ =>
  exists head::s,  t
  simp only [cons_append, append_assoc, ← P]
State after:
no goals

State before:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
s t : List α
P : s ++ l ++ t = tail
⊢ ∃ s t, s ++ l ++ t = head :: tail
Tactic:
exists head::s,  t
State after:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
s t : List α
P : s ++ l ++ t = tail
⊢ head :: s ++ l ++ t = head :: tail

State before:
α : Type u_1
head : α
l tail : List α
h : ∃ s t, s ++ l ++ t = tail
s t : List α
P : s ++ l ++ t = tail
⊢ head :: s ++ l ++ t = head :: tail
Tactic:
simp only [cons_append, append_assoc, ← P]
State after:
no goals