no goals
α✝ : Type u_1
l l₁ : List α✝
a : α✝
l₂ : List α✝
h : l <+ l₁ ++ a :: l₂
⊢ l <+ l₁ ++ l₂ ∨ a ∈ l
induction l₁ generalizing l with
| nil => match h with
  | .cons _ h => exact .inl h
  | .cons₂ _ h => exact .inr (.head ..)
| cons b l₁ IH =>
  match h with
  | .cons _ h => exact (IH h).imp_left (Sublist.cons _)
  | .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)
no goals
case nil
α✝ : Type u_1
a : α✝
l₂ l : List α✝
h : l <+ [] ++ a :: l₂
⊢ l <+ [] ++ l₂ ∨ a ∈ l
match h with
| .cons _ h => exact .inl h
| .cons₂ _ h => exact .inr (.head ..)
no goals
α✝ : Type u_1
a : α✝
l₂ l✝ : List α✝
h✝ : l✝ <+ [] ++ a :: l₂
l : List α✝
h : l <+ l₂
⊢ l <+ [] ++ l₂ ∨ a ∈ l
exact .inl h
no goals
α✝ : Type u_1
a : α✝
l₂ l : List α✝
h✝ : l <+ [] ++ a :: l₂
l₁✝ : List α✝
h : l₁✝ <+ l₂
⊢ a :: l₁✝ <+ [] ++ l₂ ∨ a ∈ a :: l₁✝
exact .inr (.head ..)
no goals
case cons
α✝ : Type u_1
a : α✝
l₂ : List α✝
b : α✝
l₁ : List α✝
IH : ∀ {l : List α✝}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
l : List α✝
h : l <+ b :: l₁ ++ a :: l₂
⊢ l <+ b :: l₁ ++ l₂ ∨ a ∈ l
match h with
| .cons _ h => exact (IH h).imp_left (Sublist.cons _)
| .cons₂ _ h => exact (IH h).imp (Sublist.cons₂ _) (.tail _)
no goals
α✝ : Type u_1
a : α✝
l₂ : List α✝
b : α✝
l₁ : List α✝
IH : ∀ {l : List α✝}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
l✝ : List α✝
h✝ : l✝ <+ b :: l₁ ++ a :: l₂
l : List α✝
h : l <+ List.append l₁ (a :: l₂)
⊢ l <+ b :: l₁ ++ l₂ ∨ a ∈ l
exact (IH h).imp_left (Sublist.cons _)
no goals
α✝ : Type u_1
a : α✝
l₂ : List α✝
b : α✝
l₁ : List α✝
IH : ∀ {l : List α✝}, l <+ l₁ ++ a :: l₂ → l <+ l₁ ++ l₂ ∨ a ∈ l
l : List α✝
h✝ : l <+ b :: l₁ ++ a :: l₂
l₁✝ : List α✝
h : l₁✝ <+ List.append l₁ (a :: l₂)
⊢ b :: l₁✝ <+ b :: l₁ ++ l₂ ∨ a ∈ b :: l₁✝
exact (IH h).imp (Sublist.cons₂ _) (.tail _)