-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem exists_perm_sublist {l₁ l₂ l₂' : List α} (s : l₁ <+ l₂) (p : l₂ ~ l₂') :
    ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂'

Proof state:
α : Type u_1
l₂ l₂' : List α
x y : α
l' l₁ : List α
s✝ : l₁ <+ y :: x :: l'
l₁✝ : List α
s : l₁✝ <+ l'
⊢ ∃ l₁', l₁' ~ y :: l₁✝ ∧ l₁' <+ x :: y :: l'

Tactic:
exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩

Result:
no goals

Proof state:
case trans
α : Type u_1
l₂ l₂' l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
IH₂ : ∀ {l₁ : List α}, l₁ <+ l₂✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝
l₁ : List α
s : l₁ <+ l₁✝
m₁ : List α
pm : m₁ ~ l₁
sm : m₁ <+ l₂✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝

Tactic:
let ⟨r₁, pr, sr⟩ := IH₂ sm

Result:
case trans
α : Type u_1
l₂ l₂' l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
IH₂ : ∀ {l₁ : List α}, l₁ <+ l₂✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝
l₁ : List α
s : l₁ <+ l₁✝
m₁ : List α
pm : m₁ ~ l₁
sm : m₁ <+ l₂✝
r₁ : List α
pr : r₁ ~ m₁
sr : r₁ <+ l₃✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝

Proof state:
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝¹ l₂✝ : List α
a✝ : l₁✝¹ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝¹ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁✝ : List α
s✝ : l₁✝ <+ x :: l₁✝¹
l₁ : List α
s : l₁ <+ l₁✝¹
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ x :: l₂✝

Tactic:
let ⟨l₁', p', s'⟩ := IH s

Result:
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝¹ l₂✝ : List α
a✝ : l₁✝¹ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝¹ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁✝ : List α
s✝ : l₁✝ <+ x :: l₁✝¹
l₁ : List α
s : l₁ <+ l₁✝¹
l₁' : List α
p' : l₁' ~ l₁
s' : l₁' <+ l₂✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ x :: l₂✝

Proof state:
case trans
α : Type u_1
l₂ l₂' l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
IH₂ : ∀ {l₁ : List α}, l₁ <+ l₂✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝
l₁ : List α
s : l₁ <+ l₁✝
m₁ : List α
pm : m₁ ~ l₁
sm : m₁ <+ l₂✝
r₁ : List α
pr : r₁ ~ m₁
sr : r₁ <+ l₃✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝

Tactic:
exact ⟨r₁, pr.trans pm, sr⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝¹ l₂✝ : List α
a✝ : l₁✝¹ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝¹ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁ : List α
s✝ : l₁ <+ x :: l₁✝¹
l₁✝ : List α
s : l₁✝ <+ l₁✝¹
⊢ ∃ l₁', l₁' ~ x :: l₁✝ ∧ l₁' <+ x :: l₂✝

Tactic:
let ⟨l₁', p', s'⟩ := IH s

Result:
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝¹ l₂✝ : List α
a✝ : l₁✝¹ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝¹ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁ : List α
s✝ : l₁ <+ x :: l₁✝¹
l₁✝ : List α
s : l₁✝ <+ l₁✝¹
l₁' : List α
p' : l₁' ~ l₁✝
s' : l₁' <+ l₂✝
⊢ ∃ l₁', l₁' ~ x :: l₁✝ ∧ l₁' <+ x :: l₂✝

Proof state:
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝¹ l₂✝ : List α
a✝ : l₁✝¹ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝¹ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁✝ : List α
s✝ : l₁✝ <+ x :: l₁✝¹
l₁ : List α
s : l₁ <+ l₁✝¹
l₁' : List α
p' : l₁' ~ l₁
s' : l₁' <+ l₂✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ x :: l₂✝

Tactic:
exact ⟨l₁', p', s'.cons _⟩

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l₂' : List α
s : l₁ <+ l₂
p : l₂ ~ l₂'
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂'

Tactic:
induction p generalizing l₁ with
| nil => exact ⟨[], sublist_nil.mp s ▸ .rfl, nil_sublist _⟩
| cons x _ IH =>
  match s with
  | .cons _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨l₁', p', s'.cons _⟩
  | .cons₂ _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩
| swap x y l' =>
  match s with
  | .cons _ (.cons _ s) => exact ⟨_, .rfl, (s.cons _).cons _⟩
  | .cons _ (.cons₂ _ s) => exact ⟨x :: _, .rfl, (s.cons _).cons₂ _⟩
  | .cons₂ _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩
  | .cons₂ _ (.cons₂ _ s) => exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩
| trans _ _ IH₁ IH₂ =>
  let ⟨m₁, pm, sm⟩ := IH₁ s
  let ⟨r₁, pr, sr⟩ := IH₂ sm
  exact ⟨r₁, pr.trans pm, sr⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ l₂' : List α
x y : α
l' l₁✝ : List α
s✝ : l₁✝ <+ y :: x :: l'
l₁ : List α
s : l₁ <+ l'
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ x :: y :: l'

Tactic:
exact ⟨_, .rfl, (s.cons _).cons _⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝¹ l₂✝ : List α
a✝ : l₁✝¹ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝¹ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁ : List α
s✝ : l₁ <+ x :: l₁✝¹
l₁✝ : List α
s : l₁✝ <+ l₁✝¹
l₁' : List α
p' : l₁' ~ l₁✝
s' : l₁' <+ l₂✝
⊢ ∃ l₁', l₁' ~ x :: l₁✝ ∧ l₁' <+ x :: l₂✝

Tactic:
exact ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
l₂ l₂' l₁ : List α
s : l₁ <+ []
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ []

Tactic:
exact ⟨[], sublist_nil.mp s ▸ .rfl, nil_sublist _⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ l₂' : List α
x y : α
l' l₁ : List α
s✝ : l₁ <+ y :: x :: l'
tail✝ : List α
s : tail✝ <+ l'
⊢ ∃ l₁', l₁' ~ y :: x :: tail✝ ∧ l₁' <+ x :: y :: l'

Tactic:
exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
l₂ l₂' : List α
x : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
l₁ : List α
s : l₁ <+ x :: l₁✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ x :: l₂✝

Tactic:
match s with
| .cons _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨l₁', p', s'.cons _⟩
| .cons₂ _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩

Result:
no goals

Proof state:
α : Type u_1
l₂ l₂' : List α
x y : α
l' l₁ : List α
s✝ : l₁ <+ y :: x :: l'
tail✝ : List α
s : tail✝ <+ l'
⊢ ∃ l₁', l₁' ~ x :: tail✝ ∧ l₁' <+ x :: y :: l'

Tactic:
exact ⟨x :: _, .rfl, (s.cons _).cons₂ _⟩

Result:
no goals

Proof state:
case trans
α : Type u_1
l₂ l₂' l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
IH₂ : ∀ {l₁ : List α}, l₁ <+ l₂✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝
l₁ : List α
s : l₁ <+ l₁✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝

Tactic:
let ⟨m₁, pm, sm⟩ := IH₁ s

Result:
case trans
α : Type u_1
l₂ l₂' l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : ∀ {l₁ : List α}, l₁ <+ l₁✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂✝
IH₂ : ∀ {l₁ : List α}, l₁ <+ l₂✝ → ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝
l₁ : List α
s : l₁ <+ l₁✝
m₁ : List α
pm : m₁ ~ l₁
sm : m₁ <+ l₂✝
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₃✝

Proof state:
case swap
α : Type u_1
l₂ l₂' : List α
x y : α
l' l₁ : List α
s : l₁ <+ y :: x :: l'
⊢ ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ x :: y :: l'

Tactic:
match s with
| .cons _ (.cons _ s) => exact ⟨_, .rfl, (s.cons _).cons _⟩
| .cons _ (.cons₂ _ s) => exact ⟨x :: _, .rfl, (s.cons _).cons₂ _⟩
| .cons₂ _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩
| .cons₂ _ (.cons₂ _ s) => exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩

Result:
no goals