-- Mathlib/Data/List/Sort.lean
theorem eq_of_perm_of_sorted [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ ~ l₂) (hs₁ : Sorted r l₁)
    (hs₂ : Sorted r l₂) : l₁ = l₂

Proof state:
case cons.intro.intro.e_a
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ = u₂ ++ [a]

Tactic:
have : ∀ x ∈ u₂, x = a := fun x m =>
  antisymm ((pairwise_append.1 hs₂).2.2 _ m a (mem_cons_self _ _)) (h₁ _ (by simp [m]))

Result:
case cons.intro.intro.e_a
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ x ∈ u₂, x = a
⊢ a :: u₂ = u₂ ++ [a]

Proof state:
case nil
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ l₂ : List α
hp : [] ~ l₂
hs₂ : Sorted r l₂
⊢ [] = l₂

Tactic:
exact hp.nil_eq

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: (u₂ ++ v₂) = u₂ ++ a :: v₂

Tactic:
change a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)

Result:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)

Proof state:
case cons.intro.intro.e_a
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ x ∈ u₂, x = a
⊢ a :: u₂ = u₂ ++ [a]

Tactic:
rw [(@eq_replicate_iff _ a (length u₂ + 1) (a :: u₂)).2,
    (@eq_replicate_iff _ a (length u₂ + 1) (u₂ ++ [a])).2] <;>
    constructor <;>
  simp [iff_true_intro this, or_comm]

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)

Tactic:
rw [← append_assoc]

Result:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ [a] ++ v₂

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
hp : a :: l₁ ~ l₂
hs₂ : Sorted r l₂
this : a ∈ l₂
⊢ a :: l₁ = l₂

Tactic:
rcases append_of_mem this with ⟨u₂, v₂, rfl⟩

Result:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
hp : a :: l₁ ~ u₂ ++ a :: v₂
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
⊢ a :: l₁ = u₂ ++ a :: v₂

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
x : α
m : x ∈ u₂
⊢ x ∈ u₂ ++ v₂

Tactic:
simp [m]

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ [a] ++ v₂

Tactic:
congr

Result:
case cons.intro.intro.e_a
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ = u₂ ++ [a]

Proof state:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
hp : a :: l₁ ~ u₂ ++ a :: v₂
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
hp' : l₁ ~ u₂ ++ v₂
⊢ a :: l₁ = u₂ ++ a :: v₂

Tactic:
obtain rfl := IH hp' (hs₂.sublist <| by simp)

Result:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ : List α
a : α
u₂ v₂ : List α
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ a' ∈ u₂ ++ v₂, r a a'
hs₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
hp : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
hp' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: (u₂ ++ v₂) = u₂ ++ a :: v₂

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
hp : a :: l₁ ~ l₂
hs₂ : Sorted r l₂
⊢ a :: l₁ = l₂

Tactic:
have : a ∈ l₂ := hp.subset (mem_cons_self _ _)

Result:
case cons
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
hp : a :: l₁ ~ l₂
hs₂ : Sorted r l₂
this : a ∈ l₂
⊢ a :: l₁ = l₂

Proof state:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
hp : a :: l₁ ~ u₂ ++ a :: v₂
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
⊢ a :: l₁ = u₂ ++ a :: v₂

Tactic:
have hp' := (perm_cons a).1 (hp.trans perm_middle)

Result:
case cons.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁✝ : List α
a : α
l₁ : List α
h₁ : ∀ a' ∈ l₁, r a a'
hs₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
hp : a :: l₁ ~ u₂ ++ a :: v₂
hs₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
hp' : l₁ ~ u₂ ++ v₂
⊢ a :: l₁ = u₂ ++ a :: v₂