-- 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 rel.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₁✝ : List α
a : α
b : List α
hab : a₁✝ < a
c : α
l₁ : List α
h₁ : c :: l₁ ≤ a₁✝ :: l₁✝
⊢ c :: l₁ < a :: b

Tactic:
apply Lex.rel

Result:
case rel.cons.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₁ : c :: l₁ ≤ a₁✝ :: l₁✝
⊢ c < a

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

Tactic:
exact Lex.rel (Decidable.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))

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
h₂ : ¬c < a
⊢ False

Tactic:
have := i₃.trans h₁ 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
this : ¬a₁✝ < a
⊢ False

Proof state:
case rel
α : 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₂✝ : α
l₂✝ : List α
hab : a₁✝ < a₂✝
l₁ : List α
h₁ : l₁ ≤ a₁✝ :: l₁✝
⊢ l₁ < a₂✝ :: l₂✝

Tactic:
rename_i a b

Result:
case rel
α : 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
l₁ : List α
h₁ : l₁ ≤ a₁✝ :: l₁✝
⊢ l₁ < a :: b

Proof state:
case rel.cons.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

Tactic:
apply Decidable.byContradiction

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
⊢ ¬c < a → False

Proof state:
case 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✝ l₁ : List α
h₁ : l₁ ≤ []
⊢ l₁ < a✝ :: l✝

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.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 : α
as bs : List α
w₃ : Lex (fun x1 x2 => x1 < x2) as bs
ih : ∀ {l₁ : List α}, l₁ ≤ as → l₁ < bs
h₁ : [] ≤ a :: as
⊢ [] < a :: bs

Tactic:
simp_all

Result:
no goals

Proof state:
case rel
α : 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
l₁ : List α
h₁ : l₁ ≤ a₁✝ :: l₁✝
⊢ l₁ < a :: b

Tactic:
cases l₁ with
| nil => simp_all
| cons c l₁ =>
  apply Lex.rel
  replace h₁ := not_lt_of_cons_le_cons h₁
  apply Decidable.byContradiction
  intro h₂
  have := i₃.trans h₁ h₂
  contradiction

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
h₂ : ¬c < a
this : ¬a₁✝ < a
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case rel.cons.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₁ : c :: l₁ ≤ a₁✝ :: l₁✝
⊢ c < a

Tactic:
replace h₁ := not_lt_of_cons_le_cons h₁

Result:
case rel.cons.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