-- Mathlib/Data/List/Sort.lean
theorem orderedInsert_erase [DecidableEq α] [IsAntisymm α r] (x : α) (xs : List α) (hx : x ∈ xs)
    (hxs : Sorted r xs) :
    (xs.erase x).orderedInsert r x = xs

Proof state:
case cons.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ y :: ys
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Tactic:
rw [mem_cons] at hx

Result:
case cons.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x = y ∨ x ∈ ys
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Proof state:
case cons.inl.cons
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
x z : α
zs : List α
ih : ∀ x ∈ z :: zs, Sorted r (z :: zs) → orderedInsert r x ((z :: zs).erase x) = z :: zs
hx : x ∈ x :: z :: zs
hxs : (∀ b ∈ z :: zs, r x b) ∧ Sorted r (z :: zs)
⊢ orderedInsert r x (z :: zs) = x :: z :: zs

Tactic:
rw [orderedInsert, if_pos (hxs.1 _ (.head zs))]

Result:
no goals

Proof state:
case cons.inr.hnc
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
hx : x ∈ ys
hrxy : r x y
⊢ x = y

Tactic:
exact antisymm hrxy (hxs.1 _ hx)

Result:
no goals

Proof state:
case cons.inl.nil
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
x : α
ih : ∀ x ∈ [], Sorted r [] → orderedInsert r x ([].erase x) = []
hx : x ∈ [x]
hxs : (∀ b ∈ [], r x b) ∧ Sorted r []
⊢ orderedInsert r x [] = [x]

Tactic:
rfl

Result:
no goals

Proof state:
case cons.inr.hnc
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
hx : x ∈ ys
⊢ ¬r x y

Tactic:
refine mt (fun hrxy => ?_) hxy

Result:
case cons.inr.hnc
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
hx : x ∈ ys
hrxy : r x y
⊢ x = y

Proof state:
case cons.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ x :: ys
hxs : (∀ b ∈ ys, r x b) ∧ Sorted r ys
⊢ orderedInsert r x ys = x :: ys

Tactic:
cases ys with
| nil => rfl
| cons z zs =>
  rw [orderedInsert, if_pos (hxs.1 _ (.head zs))]

Result:
no goals

Proof state:
case cons.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x = y ∨ x ∈ ys
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Tactic:
replace hx := hx.resolve_left hxy

Result:
case cons.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
hx : x ∈ ys
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ y :: ys
hxs : Sorted r (y :: ys)
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Tactic:
rw [sorted_cons] at hxs

Result:
case cons
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ y :: ys
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Proof state:
case cons.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ x :: ys
hxs : (∀ b ∈ ys, r x b) ∧ Sorted r ys
⊢ orderedInsert r x ((x :: ys).erase x) = x :: ys

Tactic:
rw [erase_cons_head]

Result:
case cons.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ x :: ys
hxs : (∀ b ∈ ys, r x b) ∧ Sorted r ys
⊢ orderedInsert r x ys = x :: ys

Proof state:
case nil
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
x : α
hx : x ∈ []
hxs : Sorted r []
⊢ orderedInsert r x ([].erase x) = []

Tactic:
cases hx

Result:
no goals

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ y :: ys
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Tactic:
obtain rfl | hxy := Decidable.eq_or_ne x y

Result:
case cons.inl
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ x :: ys
hxs : (∀ b ∈ ys, r x b) ∧ Sorted r ys
⊢ orderedInsert r x ((x :: ys).erase x) = x :: ys

case cons.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hx : x ∈ y :: ys
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Proof state:
case cons.inr
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
hx : x ∈ ys
⊢ orderedInsert r x ((y :: ys).erase x) = y :: ys

Tactic:
rw [erase_cons_tail (not_beq_of_ne hxy.symm), orderedInsert, ih _ hx hxs.2, if_neg]

Result:
case cons.inr.hnc
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsAntisymm α r
y : α
ys : List α
ih : ∀ x ∈ ys, Sorted r ys → orderedInsert r x (ys.erase x) = ys
x : α
hxs : (∀ b ∈ ys, r y b) ∧ Sorted r ys
hxy : x ≠ y
hx : x ∈ ys
⊢ ¬r x y