no goals
α : Type u_1
β : Type ?u.37187
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
s : List α
⊢ s ∈ tails [] ↔ s <:+ []
simp only [tails, mem_singleton, suffix_nil]
α : Type u_1
β : Type ?u.37187
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
α : Type u_1
β : Type ?u.37187
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s ∈ tails (a :: t) ↔ s <:+ a :: t
simp only [tails, mem_cons, mem_tails s t]
no goals
α : Type u_1
β : Type ?u.37187
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
exact
  show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
    ⟨fun o =>
      match s, t, o with
      | _, t, Or.inl rfl => suffix_rfl
      | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
      fun e =>
      match s, t, e with
      | _, t, ⟨[], rfl⟩ => Or.inl rfl
      | s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩