-- Mathlib/Data/List/Chain.lean
theorem Chain'.cons_of_le [LinearOrder α] {a : α} {as m : List α}
    (ha : List.Chain' (· > ·) (a :: as)) (hm : List.Chain' (· > ·) m) (hmas : m ≤ as) :
    List.Chain' (· > ·) (a :: m)

Proof state:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : ¬a' :: as ≤ b :: bs
hh : a' < b
⊢ a' :: as ≤ b :: bs

Tactic:
apply le_of_lt

Result:
case cons.cons.inl.hab
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : ¬a' :: as ≤ b :: bs
hh : a' < b
⊢ a' :: as < b :: bs

Proof state:
case cons
α : Type u
inst✝ : LinearOrder α
a : α
as : List α
ha : Chain' (fun x1 x2 => x1 > x2) (a :: as)
b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ Chain' (fun x1 x2 => x1 > x2) (a :: b :: bs)

Tactic:
apply hm.cons

Result:
case cons
α : Type u
inst✝ : LinearOrder α
a : α
as : List α
ha : Chain' (fun x1 x2 => x1 > x2) (a :: as)
b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ a > b

Proof state:
case cons.cons.inl.hab
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : ¬a' :: as ≤ b :: bs
hh : a' < b
⊢ a' :: as < b :: bs

Tactic:
exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel hh)

Result:
no goals

Proof state:
case cons.cons.inr
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ a' ≥ b

Tactic:
simp_all only [List.cons.injEq, le_refl]

Result:
no goals

Proof state:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a' ≥ b

Tactic:
rw [le_iff_lt_or_eq] at hmas

Result:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as ∨ b :: bs = a' :: as
⊢ a' ≥ b

Proof state:
case cons.nil
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
ha : Chain' (fun x1 x2 => x1 > x2) [a]
hmas : b :: bs ≤ []
⊢ a > b

Tactic:
simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas

Result:
case cons.nil
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
ha : Chain' (fun x1 x2 => x1 > x2) [a]
hmas : b :: bs < []
⊢ a > b

Proof state:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : ¬a' :: as ≤ b :: bs
hh : a' < b
⊢ False

Tactic:
apply hmas

Result:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : ¬a' :: as ≤ b :: bs
hh : a' < b
⊢ a' :: as ≤ b :: bs

Proof state:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as ∨ b :: bs = a' :: as
⊢ a' ≥ b

Tactic:
rcases hmas with hmas | hmas

Result:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ a' ≥ b

case cons.cons.inr
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ a' ≥ b

Proof state:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : Chain' (fun x1 x2 => x1 > x2) (a :: a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b

Tactic:
rw [List.chain'_cons] at ha

Result:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b

Proof state:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b

Tactic:
refine gt_of_gt_of_ge ha.1 ?_

Result:
case cons.cons
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a' ≥ b

Proof state:
case nil
α : Type u
inst✝ : LinearOrder α
a : α
as : List α
ha : Chain' (fun x1 x2 => x1 > x2) (a :: as)
hm : Chain' (fun x1 x2 => x1 > x2) []
hmas : [] ≤ as
⊢ Chain' (fun x1 x2 => x1 > x2) [a]

Tactic:
simp only [List.chain'_singleton]

Result:
no goals

Proof state:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ a' ≥ b

Tactic:
by_contra! hh

Result:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
hh : a' < b
⊢ False

Proof state:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
hh : a' < b
⊢ False

Tactic:
rw [← not_le] at hmas

Result:
case cons.cons.inl
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ Chain' (fun x1 x2 => x1 > x2) (a' :: as)
hmas : ¬a' :: as ≤ b :: bs
hh : a' < b
⊢ False

Proof state:
case cons.nil
α : Type u
inst✝ : LinearOrder α
a b : α
bs : List α
hm : Chain' (fun x1 x2 => x1 > x2) (b :: bs)
ha : Chain' (fun x1 x2 => x1 > x2) [a]
hmas : b :: bs < []
⊢ a > b

Tactic:
exact (List.not_lt_nil _ hmas).elim

Result:
no goals