-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.eq_of_sorted : ∀ {l₁ l₂ : List α}
    (_ : ∀ a b, a ∈ l₁ → b ∈ l₂ → le a b → le b a → a = b)
    (_ : l₁.Pairwise le) (_ : l₂.Pairwise le) (_ : l₁ ~ l₂), l₁ = l₂
  | [], [], _, _, _, _ => rfl
  | [], b :: l₂, _, _, _, h => by simp_all
  | a :: l₁, [], _, _, _, h => by simp_all
  | a :: l₁, b :: l₂, w, h₁, h₂, h => by
    have am : a ∈ b :: l₂ := h.subset (mem_cons_self _ _)
    have bm : b ∈ a :: l₁ := h.symm.subset (mem_cons_self _ _)
    have ab : a = b

Proof state:
case inr
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ l₂
bm : b = a ∨ b ∈ l₁
⊢ a = b

Tactic:
rcases bm with rfl | bm

Result:
case inr.inl
α : Type u_1
le : α → α → Prop
l₁ : List α
b : α
l₂ : List α
h₂ : Pairwise le (b :: l₂)
w : ∀ (a b_1 : α), a ∈ b :: l₁ → b_1 ∈ b :: l₂ → le a b_1 → le b_1 a → a = b_1
h₁ : Pairwise le (b :: l₁)
h : b :: l₁ ~ b :: l₂
am : b ∈ l₂
⊢ b = b

case inr.inr
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ l₂
bm : b ∈ l₁
⊢ a = b

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ b :: l₂
bm : b ∈ a :: l₁
⊢ a = b

Tactic:
simp only [mem_cons] at am

Result:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
bm : b ∈ a :: l₁
am : a = b ∨ a ∈ l₂
⊢ a = b

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ b :: l₂
⊢ a :: l₁ = b :: l₂

Tactic:
have bm : b ∈ a :: l₁ := h.symm.subset (mem_cons_self _ _)

Result:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ b :: l₂
bm : b ∈ a :: l₁
⊢ a :: l₁ = b :: l₂

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
⊢ a :: l₁ = b :: l₂

Tactic:
have am : a ∈ b :: l₂ := h.subset (mem_cons_self _ _)

Result:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ b :: l₂
⊢ a :: l₁ = b :: l₂

Proof state:
case inr.inl
α : Type u_1
le : α → α → Prop
l₁ : List α
b : α
l₂ : List α
h₂ : Pairwise le (b :: l₂)
w : ∀ (a b_1 : α), a ∈ b :: l₁ → b_1 ∈ b :: l₂ → le a b_1 → le b_1 a → a = b_1
h₁ : Pairwise le (b :: l₁)
h : b :: l₁ ~ b :: l₂
am : b ∈ l₂
⊢ b = b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
am : a ∈ a :: l₂
bm : a ∈ a :: l₁
h : l₁ ~ l₂
this : l₁ = l₂
⊢ a :: l₁ = a :: l₂

Tactic:
simp_all

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ l₂
bm : b ∈ l₁
⊢ a = b

Tactic:
exact w _ _ (mem_cons_self _ _) (mem_cons_self _ _)
  (rel_of_pairwise_cons h₁ bm) (rel_of_pairwise_cons h₂ am)

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
bm : b ∈ a :: l₁
am : a = b ∨ a ∈ l₂
⊢ a = b

Tactic:
rcases am with rfl | am

Result:
case inl
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
h : a :: l₁ ~ a :: l₂
bm : a ∈ a :: l₁
⊢ a = a

case inr
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
bm : b ∈ a :: l₁
am : a ∈ l₂
⊢ a = b

Proof state:
α : Type u_1
le : α → α → Prop
b : α
l₂ : List α
x✝² : ∀ (a b_1 : α), a ∈ [] → b_1 ∈ b :: l₂ → le a b_1 → le b_1 a → a = b_1
x✝¹ : Pairwise le []
x✝ : Pairwise le (b :: l₂)
h : [] ~ b :: l₂
⊢ [] = b :: l₂

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
x✝² : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ [] → le a_1 b → le b a_1 → a_1 = b
x✝¹ : Pairwise le (a :: l₁)
x✝ : Pairwise le []
h : a :: l₁ ~ []
⊢ a :: l₁ = []

Tactic:
simp_all

Result:
no goals

Proof state:
case inl
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
h : a :: l₁ ~ a :: l₂
bm : a ∈ a :: l₁
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
am : a ∈ a :: l₂
bm : a ∈ a :: l₁
h : l₁ ~ l₂
⊢ a :: l₁ = a :: l₂

Tactic:
have := Perm.eq_of_sorted
  (fun x y hx hy => w x y (mem_cons_of_mem a hx) (mem_cons_of_mem a hy))
  h₁.tail h₂.tail h

Result:
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
am : a ∈ a :: l₂
bm : a ∈ a :: l₁
h : l₁ ~ l₂
this : l₁ = l₂
⊢ a :: l₁ = a :: l₂

Proof state:
case inr
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
bm : b ∈ a :: l₁
am : a ∈ l₂
⊢ a = b

Tactic:
simp only [mem_cons] at bm

Result:
case inr
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ l₂
bm : b = a ∨ b ∈ l₁
⊢ a = b

Proof state:
α : Type u_1
le : α → α → Prop
a : α
l₁ : List α
b : α
l₂ : List α
w : ∀ (a_1 b_1 : α), a_1 ∈ a :: l₁ → b_1 ∈ b :: l₂ → le a_1 b_1 → le b_1 a_1 → a_1 = b_1
h₁ : Pairwise le (a :: l₁)
h₂ : Pairwise le (b :: l₂)
h : a :: l₁ ~ b :: l₂
am : a ∈ b :: l₂
bm : b ∈ a :: l₁
ab : a = b
⊢ a :: l₁ = b :: l₂

Tactic:
subst ab

Result:
α : Type u_1
le : α → α → Prop
a : α
l₁ l₂ : List α
h₁ : Pairwise le (a :: l₁)
w : ∀ (a_1 b : α), a_1 ∈ a :: l₁ → b ∈ a :: l₂ → le a_1 b → le b a_1 → a_1 = b
h₂ : Pairwise le (a :: l₂)
h : a :: l₁ ~ a :: l₂
am : a ∈ a :: l₂
bm : a ∈ a :: l₁
⊢ a :: l₁ = a :: l₂