no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' l₁ : List α
s : l₁ <+ []
⊢ ∃ l₁' x, l₁' <+ []
exact ⟨[], eq_nil_of_sublist_nil s ▸ Perm.refl _, nil_sublist _⟩
case cons.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₂ l₂' : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁' x, l₁' <+ l₂✝
l₁ : List α
s : l₁ <+ l₁✝
⊢ ∃ l₁' x_1, l₁' <+ x :: l₂✝

case cons.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₂ l₂' : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁' x, l₁' <+ l₂✝
l₁ : List α
s : l₁ <+ l₁✝
⊢ ∃ l₁' x_1, l₁' <+ x :: l₂✝
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₂ l₂' : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁' x, l₁' <+ l₂✝
l₁ : List α
s : l₁ <+ x :: l₁✝
⊢ ∃ l₁' x_1, l₁' <+ x :: l₂✝
cases' s with _ _ _ s l₁ _ _ s
no goals
case cons.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₂ l₂' : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁' x, l₁' <+ l₂✝
l₁ : List α
s : l₁ <+ l₁✝
⊢ ∃ l₁' x_1, l₁' <+ x :: l₂✝
exact
  let ⟨l₁', p', s'⟩ := IH s
  ⟨l₁', p', s'.cons _⟩
no goals
case cons.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₂ l₂' : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁' x, l₁' <+ l₂✝
l₁ : List α
s : l₁ <+ l₁✝
⊢ ∃ l₁' x_1, l₁' <+ x :: l₂✝
exact
  let ⟨l₁', p', s'⟩ := IH s
  ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩
case swap.cons.cons
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝

case swap.cons.cons₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝

case swap.cons₂.cons
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝

case swap.cons₂.cons₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ y :: x :: l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝
cases' s with _ _ _ s l₁ _ _ s <;> cases' s with _ _ _ s l₁ _ _ s
no goals
case swap.cons.cons
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝
exact ⟨l₁, Perm.refl _, (s.cons _).cons _⟩
no goals
case swap.cons.cons₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝
exact ⟨x :: l₁, Perm.refl _, (s.cons _).cons₂ _⟩
no goals
case swap.cons₂.cons
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝
exact ⟨y :: l₁, Perm.refl _, (s.cons₂ _).cons _⟩
no goals
case swap.cons₂.cons₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₂ l₂' : List α
x y : α
l✝ l₁ : List α
s : l₁ <+ l✝
⊢ ∃ l₁' x_1, l₁' <+ x :: y :: l✝
exact ⟨x :: y :: l₁, Perm.swap _ _ _, (s.cons₂ _).cons₂ _⟩
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₂ l₂' l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁' x, l₁' <+ l₂✝
IH₂ : ∀ {l₁ : List α}, l₁ <+ l₂✝ → ∃ l₁' x, l₁' <+ l₃✝
l₁ : List α
s : l₁ <+ l₁✝
⊢ ∃ l₁' x, l₁' <+ l₃✝
exact
  let ⟨m₁, pm, sm⟩ := IH₁ s
  let ⟨r₁, pr, sr⟩ := IH₂ sm
  ⟨r₁, pr.trans pm, sr⟩