-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
    [i₁ : Std.Asymm (· < · : α → α → Prop)]
    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
    [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
    {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃

Proof state:
case cons.cons
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a :: as
⊢ c :: l₁ < a :: bs

Tactic:
have w₄ := not_lt_of_cons_le_cons h₁

Result:
case cons.cons
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a :: as
w₄ : ¬a < c
⊢ c :: l₁ < a :: bs

Proof state:
case cons.cons
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a :: as
w₄ : ¬a < c
⊢ c :: l₁ < a :: bs

Tactic:
by_cases w₅ : a = c

Result:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a :: as
w₄ : ¬a < c
w₅ : a = c
⊢ c :: l₁ < a :: bs

case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a :: as
w₄ : ¬a < c
w₅ : ¬a = c
⊢ c :: l₁ < a :: bs

Proof state:
case cons
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a✝ : α
l₁✝ l₂✝ : List α
w₃ : Lex (fun x1 x2 => x1 < x2) l₁✝ l₂✝
ih : ∀ {l₁ : List α}, l₁ ≤ l₁✝ → l₁ < l₂✝
l₁ : List α
h₁ : l₁ ≤ a✝ :: l₁✝
⊢ l₁ < a✝ :: l₂✝

Tactic:
rename_i a as bs

Result:
case cons
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
l₁ : List α
h₁ : l₁ ≤ a :: as
⊢ l₁ < a :: bs

Proof state:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a :: as
w₄ : ¬a < c
w₅ : a = c
⊢ c :: l₁ < a :: bs

Tactic:
subst w₅

Result:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
l₁ : List α
h₁ : a :: l₁ ≤ a :: as
w₄ : ¬a < a
⊢ a :: l₁ < a :: bs

Proof state:
case rel.nil
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a₁✝ : α
l₁✝ : List α
a : α
b : List α
hab : a₁✝ < a
h₁ : [] ≤ a₁✝ :: l₁✝
⊢ [] < a :: b

Tactic:
simp_all

Result:
no goals

Proof state:
case rel.cons.h.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a₁✝ : α
l₁✝ : List α
a : α
b : List α
hab : a₁✝ < a
c : α
l₁ : List α
h₁ : ¬a₁✝ < c
⊢ ¬c < a → False

Tactic:
intro h₂

Result:
case rel.cons.h.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a₁✝ : α
l₁✝ : List α
a : α
b : List α
hab : a₁✝ < a
c : α
l₁ : List α
h₁ : ¬a₁✝ < c
h₂ : ¬c < a
⊢ False

Proof state:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
i₁ : Std.Asymm fun x1 x2 => x1 < x2
i₂ : Std.Antisymm fun x1 x2 => ¬x1 < x2
i₃ : Trans (fun x1 x2 => ¬x1 < x2) (fun x1 x2 => ¬x1 < x2) fun x1 x2 => ¬x1 < x2
l₂ l₃ : List α
a : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
l₁ : List α
h₁ : a :: l₁ ≤ a :: as
w₄ : ¬a < a
⊢ a :: l₁ < a :: bs

Tactic:
exact Lex.cons (ih (le_of_cons_le_cons h₁))

Result:
no goals