no goals
α : Type u_1
l₁ l₂ l₃ : List α
h₁ : l₁ <+ l₂
h₂ : l₂ <+ l₃
⊢ l₁ <+ l₃
induction h₂ generalizing l₁ with
| slnil => exact h₁
| cons _ _ IH => exact (IH h₁).cons _
| @cons₂ l₂ _ a _ IH =>
  generalize e : a :: l₂ = l₂'
  match e ▸ h₁ with
  | .slnil => apply nil_sublist
  | .cons a' h₁' => cases e; apply (IH h₁').cons
  | .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂
no goals
case slnil
α : Type u_1
l₂ l₃ l₁ : List α
h₁ : l₁ <+ []
⊢ l₁ <+ []
exact h₁
no goals
case cons
α : Type u_1
l₂ l₃ l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → l₁ <+ l₂✝
l₁ : List α
h₁ : l₁ <+ l₁✝
⊢ l₁ <+ a✝¹ :: l₂✝
exact (IH h₁).cons _
case cons₂
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁ : List α
h₁ : l₁ <+ a :: l₂
l₂' : List α
e : a :: l₂ = l₂'
⊢ l₁ <+ a :: l₂✝
case cons₂
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁ : List α
h₁ : l₁ <+ a :: l₂
⊢ l₁ <+ a :: l₂✝
generalize e : a :: l₂ = l₂'
no goals
case cons₂
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁ : List α
h₁ : l₁ <+ a :: l₂
l₂' : List α
e : a :: l₂ = l₂'
⊢ l₁ <+ a :: l₂✝
match e ▸ h₁ with
| .slnil => apply nil_sublist
| .cons a' h₁' => cases e; apply (IH h₁').cons
| .cons₂ a' h₁' => cases e; apply (IH h₁').cons₂
no goals
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
h₁ : [] <+ a :: l₂
e : a :: l₂ = []
⊢ [] <+ a :: l₂✝
apply nil_sublist
case refl
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁ : List α
h₁ : l₁ <+ a :: l₂
h₁' : l₁ <+ l₂
⊢ l₁ <+ a :: l₂✝
α : Type u_1
l₂✝² l₃ l₂ l₂✝¹ : List α
a : α
a✝ : l₂ <+ l₂✝¹
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝¹
l₁ l₂✝ : List α
a' : α
h₁' : l₁ <+ l₂✝
h₁ : l₁ <+ a :: l₂
e : a :: l₂ = a' :: l₂✝
⊢ l₁ <+ a :: l₂✝¹
cases e
no goals
case refl
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁ : List α
h₁ : l₁ <+ a :: l₂
h₁' : l₁ <+ l₂
⊢ l₁ <+ a :: l₂✝
apply (IH h₁').cons
case refl
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁✝ : List α
h₁ : a :: l₁✝ <+ a :: l₂
h₁' : l₁✝ <+ l₂
⊢ a :: l₁✝ <+ a :: l₂✝
α : Type u_1
l₂✝² l₃ l₂ l₂✝¹ : List α
a : α
a✝ : l₂ <+ l₂✝¹
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝¹
l₁✝ l₂✝ : List α
a' : α
h₁' : l₁✝ <+ l₂✝
h₁ : a' :: l₁✝ <+ a :: l₂
e : a :: l₂ = a' :: l₂✝
⊢ a' :: l₁✝ <+ a :: l₂✝¹
cases e
no goals
case refl
α : Type u_1
l₂✝¹ l₃ l₂ l₂✝ : List α
a : α
a✝ : l₂ <+ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₂ → l₁ <+ l₂✝
l₁✝ : List α
h₁ : a :: l₁✝ <+ a :: l₂
h₁' : l₁✝ <+ l₂
⊢ a :: l₁✝ <+ a :: l₂✝
apply (IH h₁').cons₂