-- Mathlib/Data/List/Sort.lean
theorem Sorted.orderedInsert (a : α) : ∀ l, Sorted r l → Sorted r (orderedInsert r a l)
  | [], _ => sorted_singleton a
  | b :: l, h => by
    by_cases h' : a ≼ b
    · -- Porting note: was
      -- `simpa [orderedInsert, h', h] using fun b' bm => trans h' (rel_of_sorted_cons h _ bm)`
      rw [List.orderedInsert, if_pos h', sorted_cons]
      exact ⟨forall_mem_cons.2 ⟨h', fun c hc => _root_.trans h' (rel_of_sorted_cons h _ hc)⟩, h⟩
    · suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
        simpa [orderedInsert, h', h.of_cons.orderedInsert a l]
      intro b' bm
      rcases (mem_orderedInsert r).mp bm with be | bm
      · subst b'
        exact (total_of r _ _).resolve_left h'
      · exact rel_of_sorted_cons h _ bm

Proof state:
case neg.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
exact rel_of_sorted_cons h _ bm

Result:
no goals

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
⊢ ∀ b' ∈ List.orderedInsert r a l, r b b'

Tactic:
intro b' bm

Result:
case neg
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
⊢ r b b'

Proof state:
case neg.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
be : b' = a
⊢ r b b'

Tactic:
subst b'

Result:
case neg.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
bm : a ∈ List.orderedInsert r a l
⊢ r b a

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
this : ∀ b' ∈ List.orderedInsert r a l, r b b'
⊢ Sorted r (List.orderedInsert r a (b :: l))

Tactic:
simpa [orderedInsert, h', h.of_cons.orderedInsert a l]

Result:
no goals

Proof state:
case neg.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
bm : a ∈ List.orderedInsert r a l
⊢ r b a

Tactic:
exact (total_of r _ _).resolve_left h'

Result:
no goals

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
⊢ Sorted r (List.orderedInsert r a (b :: l))

Tactic:
suffices ∀ b' : α, b' ∈ List.orderedInsert r a l → r b b' by
  simpa [orderedInsert, h', h.of_cons.orderedInsert a l]

Result:
case neg
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
⊢ ∀ b' ∈ List.orderedInsert r a l, r b b'

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
⊢ r b b'

Tactic:
rcases (mem_orderedInsert r).mp bm with be | bm

Result:
case neg.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
be : b' = a
⊢ r b b'

case neg.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
⊢ Sorted r (List.orderedInsert r a (b :: l))

Tactic:
by_cases h' : a ≼ b

Result:
case pos
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : r a b
⊢ Sorted r (List.orderedInsert r a (b :: l))

case neg
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : ¬r a b
⊢ Sorted r (List.orderedInsert r a (b :: l))

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : r a b
⊢ (∀ b_1 ∈ b :: l, r a b_1) ∧ Sorted r (b :: l)

Tactic:
exact ⟨forall_mem_cons.2 ⟨h', fun c hc => _root_.trans h' (rel_of_sorted_cons h _ hc)⟩, h⟩

Result:
no goals

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : r a b
⊢ Sorted r (List.orderedInsert r a (b :: l))

Tactic:
rw [List.orderedInsert, if_pos h', sorted_cons]

Result:
case pos
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : IsTotal α r
inst✝ : IsTrans α r
a b : α
l : List α
h : Sorted r (b :: l)
h' : r a b
⊢ (∀ b_1 ∈ b :: l, r a b_1) ∧ Sorted r (b :: l)