-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_trans {r : α → α → Prop}
    (lt_trans : ∀ {x y z : α}, r x y → r y z → r x z)
    (h₁ : Lex r l₁ l₂) (h₂ : Lex r l₂ l₃) : Lex r l₁ l₃

Proof state:
α : Type u_1
l₁✝ l₂✝¹ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a : α
l₁ : List α
b : α
l₂ : List α
ab : r a b
l₃ : List α
h₂ : Lex r (b :: l₂) l₃
a₂✝ : α
l₂✝ : List α
bc : r b a₂✝
⊢ Lex r (a :: l₁) (a₂✝ :: l₂✝)

Tactic:
exact List.Lex.rel (lt_trans ab bc)

Result:
no goals

Proof state:
case nil
α : Type u_1
l₁ l₂ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a✝ : α
l✝ l₃ : List α
head✝ : α
tail✝ : List α
h₂ : Lex r (a✝ :: l✝) (head✝ :: tail✝)
⊢ Lex r [] (head✝ :: tail✝)

Tactic:
exact List.Lex.nil ..

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ l₃ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
h₁ : Lex r l₁ l₂
h₂ : Lex r l₂ l₃
⊢ Lex r l₁ l₃

Tactic:
induction h₁ generalizing l₃ with
| nil => let _::_ := l₃; exact List.Lex.nil ..
| @rel a l₁ b l₂ ab =>
  match h₂ with
  | .rel bc => exact List.Lex.rel (lt_trans ab bc)
  | .cons ih =>
    exact List.Lex.rel ab
| @cons a l₁ l₂ h₁ ih2 =>
  match h₂ with
  | .rel bc =>
    exact List.Lex.rel bc
  | .cons ih =>
    exact List.Lex.cons (ih2 ih)

Result:
no goals

Proof state:
α : Type u_1
l₁✝ l₂✝¹ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a : α
l₁ l₂ : List α
h₁ : Lex r l₁ l₂
ih2 : ∀ {l₃ : List α}, Lex r l₂ l₃ → Lex r l₁ l₃
l₃ : List α
h₂ : Lex r (a :: l₂) l₃
a₂✝ : α
l₂✝ : List α
bc : r a a₂✝
⊢ Lex r (a :: l₁) (a₂✝ :: l₂✝)

Tactic:
exact List.Lex.rel bc

Result:
no goals

Proof state:
α : Type u_1
l₁✝ l₂✝¹ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a : α
l₁ l₂ : List α
h₁ : Lex r l₁ l₂
ih2 : ∀ {l₃ : List α}, Lex r l₂ l₃ → Lex r l₁ l₃
l₃ : List α
h₂ : Lex r (a :: l₂) l₃
l₂✝ : List α
ih : Lex r l₂ l₂✝
⊢ Lex r (a :: l₁) (a :: l₂✝)

Tactic:
exact List.Lex.cons (ih2 ih)

Result:
no goals

Proof state:
case rel
α : Type u_1
l₁✝ l₂✝ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a : α
l₁ : List α
b : α
l₂ : List α
ab : r a b
l₃ : List α
h₂ : Lex r (b :: l₂) l₃
⊢ Lex r (a :: l₁) l₃

Tactic:
match h₂ with
| .rel bc => exact List.Lex.rel (lt_trans ab bc)
| .cons ih =>
  exact List.Lex.rel ab

Result:
no goals

Proof state:
case nil
α : Type u_1
l₁ l₂ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a✝ : α
l✝ l₃ : List α
h₂ : Lex r (a✝ :: l✝) l₃
⊢ Lex r [] l₃

Tactic:
let _::_ := l₃

Result:
case nil
α : Type u_1
l₁ l₂ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a✝ : α
l✝ l₃ : List α
head✝ : α
tail✝ : List α
h₂ : Lex r (a✝ :: l✝) (head✝ :: tail✝)
⊢ Lex r [] (head✝ :: tail✝)

Proof state:
α : Type u_1
l₁✝ l₂✝¹ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a : α
l₁ : List α
b : α
l₂ : List α
ab : r a b
l₃ : List α
h₂ : Lex r (b :: l₂) l₃
l₂✝ : List α
ih : Lex r l₂ l₂✝
⊢ Lex r (a :: l₁) (b :: l₂✝)

Tactic:
exact List.Lex.rel ab

Result:
no goals

Proof state:
case cons
α : Type u_1
l₁✝ l₂✝ : List α
r : α → α → Prop
lt_trans : ∀ {x y z : α}, r x y → r y z → r x z
a : α
l₁ l₂ : List α
h₁ : Lex r l₁ l₂
ih2 : ∀ {l₃ : List α}, Lex r l₂ l₃ → Lex r l₁ l₃
l₃ : List α
h₂ : Lex r (a :: l₂) l₃
⊢ Lex r (a :: l₁) l₃

Tactic:
match h₂ with
| .rel bc =>
  exact List.Lex.rel bc
| .cons ih =>
  exact List.Lex.cons (ih2 ih)

Result:
no goals