-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.trans {l₁ l₂ l₃ : List α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) : l₁ <+ l₃

Proof state:
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₂✝

Tactic:
apply (IH h₁').cons

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
h₁ : l₁ <+ l₂
h₂ : l₂ <+ l₃
⊢ l₁ <+ l₃

Tactic:
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₂

Result:
no goals

Proof state:
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₂✝

Tactic:
apply (IH h₁').cons₂

Result:
no goals

Proof state:
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₂✝

Tactic:
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₂

Result:
no goals

Proof state:
α : 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₂✝¹

Tactic:
cases e

Result:
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₂✝

Proof state:
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₂✝

Tactic:
exact (IH h₁).cons _

Result:
no goals

Proof state:
α : 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₂✝

Tactic:
apply nil_sublist

Result:
no goals

Proof state:
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₂✝

Tactic:
generalize e : a :: l₂ = l₂'

Result:
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₂✝

Proof state:
case slnil
α : Type u_1
l₂ l₃ l₁ : List α
h₁ : l₁ <+ []
⊢ l₁ <+ []

Tactic:
exact h₁

Result:
no goals

Proof state:
α : 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₂✝¹

Tactic:
cases e

Result:
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₂✝