-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem List.Sorted.lt_ord_of_lt [LinearOrder α] [WellFoundedLT α] {l m : List α}
    {o : Ordinal} (hl : l.Sorted (· > ·)) (hm : m.Sorted (· > ·)) (hmltl : m < l)
    (hlt : ∀ i ∈ l, Ordinal.typein (α := α) (· < ·) i < o) :
      ∀ i ∈ m, Ordinal.typein (α := α) (· < ·) i < o

Proof state:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
refine lt_of_le_of_lt ?_ (hlt a (mem_cons_self a as))

Result:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i ≤ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding a

Proof state:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
⊢ ∀ i ∈ b :: bs, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
intro i hi

Result:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Proof state:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i ≤ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding a

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
l m : List α
o : Ordinal.{u}
hl : Sorted (fun x1 x2 => x1 > x2) l
hm : Sorted (fun x1 x2 => x1 > x2) m
hlt : ∀ i ∈ l, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
hmltl : Lex (fun x1 x2 => x1 < x2) m l
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
cases l with
| nil => simp at hmltl
| cons a as =>
  cases m with
  | nil => intro i hi; simp at hi
  | cons b bs =>
    intro i hi
    suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a (mem_cons_self a as)); simpa
    cases hi with
    | head as => exact List.head_le_of_lt hmltl
    | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_sorted_cons hm _ hi)
        (List.head_le_of_lt hmltl))

Result:
no goals

Proof state:
case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
hm : Sorted (fun x1 x2 => x1 > x2) []
hmltl : Lex (fun x1 x2 => x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
simp at hi

Result:
no goals

Proof state:
case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
hm : Sorted (fun x1 x2 => x1 > x2) []
hmltl : Lex (fun x1 x2 => x1 < x2) [] (a :: as)
⊢ ∀ i ∈ [], (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
intro i hi

Result:
case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
hm : Sorted (fun x1 x2 => x1 > x2) []
hmltl : Lex (fun x1 x2 => x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Proof state:
case cons.cons.head
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
⊢ b ≤ a

Tactic:
exact List.head_le_of_lt hmltl

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : Sorted (fun x1 x2 => x1 > x2) m
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
hmltl : Lex (fun x1 x2 => x1 < x2) m (a :: as)
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
cases m with
| nil => intro i hi; simp at hi
| cons b bs =>
  intro i hi
  suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a (mem_cons_self a as)); simpa
  cases hi with
  | head as => exact List.head_le_of_lt hmltl
  | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_sorted_cons hm _ hi)
      (List.head_le_of_lt hmltl))

Result:
no goals

Proof state:
case cons.cons.tail
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : Mem i bs
⊢ i ≤ a

Tactic:
exact le_of_lt (lt_of_lt_of_le (List.rel_of_sorted_cons hm _ hi)
(List.head_le_of_lt hmltl))

Result:
no goals

Proof state:
case nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
m : List α
o : Ordinal.{u}
hm : Sorted (fun x1 x2 => x1 > x2) m
hl : Sorted (fun x1 x2 => x1 > x2) []
hlt : ∀ i ∈ [], (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
hmltl : Lex (fun x1 x2 => x1 < x2) m []
⊢ ∀ i ∈ m, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
simp at hmltl

Result:
no goals

Proof state:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o

Tactic:
suffices h : i ≤ a by refine lt_of_le_of_lt ?_ (hlt a (mem_cons_self a as)); simpa

Result:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ i ≤ a