case nil
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
s₂✝ : Sorted r l₂✝
l₂ : List α
p : [] ~ l₂
s₂ : Sorted r l₂
⊢ [] = l₂

case cons
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
s₂✝ : Sorted r l₂✝
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
p : a :: l₁ ~ l₂
s₂ : Sorted r l₂
⊢ a :: l₁ = l₂
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p : l₁ ~ l₂
s₁ : Sorted r l₁
s₂ : Sorted r l₂
⊢ l₁ = l₂
induction' s₁ with a l₁ h₁ s₁ IH generalizing l₂
no goals
case nil
α : Type uu
r : α → α → Prop
a : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂✝ : List α
p✝ : l₁ ~ l₂✝
s₂✝ : Sorted r l₂✝
l₂ : List α
p : [] ~ l₂
s₂ : Sorted r l₂
⊢ [] = l₂
exact p.nil_eq
case cons
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
s₂✝ : Sorted r l₂✝
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
p : a :: l₁ ~ l₂
s₂ : Sorted r l₂
this : a ∈ l₂
⊢ a :: l₁ = l₂
case cons
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
s₂✝ : Sorted r l₂✝
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
p : a :: l₁ ~ l₂
s₂ : Sorted r l₂
⊢ a :: l₁ = l₂
have : a ∈ l₂ := p.subset (mem_cons_self _ _)
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
⊢ a :: l₁ = u₂ ++ a :: v₂
case cons
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂✝ : List α
p✝ : l₁✝ ~ l₂✝
s₂✝ : Sorted r l₂✝
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
l₂ : List α
p : a :: l₁ ~ l₂
s₂ : Sorted r l₂
this : a ∈ l₂
⊢ a :: l₁ = l₂
rcases mem_split this with ⟨u₂, v₂, rfl⟩
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
p' : l₁ ~ u₂ ++ v₂
⊢ a :: l₁ = u₂ ++ a :: v₂
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
⊢ a :: l₁ = u₂ ++ a :: v₂
have p' := (perm_cons a).1 (p.trans perm_middle)
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: (u₂ ++ v₂) = u₂ ++ a :: v₂
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
p' : l₁ ~ u₂ ++ v₂
⊢ a :: l₁ = u₂ ++ a :: v₂
obtain rfl := IH p' (s₂.sublist <| by simp)
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: (u₂ ++ v₂) = u₂ ++ a :: v₂
change a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ [a] ++ v₂
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)
rw [← append_assoc]
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ = u₂ ++ [a]
case cons.intro.intro
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ ++ v₂ = u₂ ++ [a] ++ v₂
congr
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ a :: u₂ = u₂ ++ [a]
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
⊢ a :: u₂ = u₂ ++ [a]
have : ∀ (x : α) (_ : x ∈ u₂), x = a := fun x m =>
  antisymm ((pairwise_append.1 s₂).2.2 _ m a (mem_cons_self _ _)) (h₁ _ (by simp [m]))
no goals
case cons.intro.intro.e_a
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this✝ : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
this : ∀ (x : α), x ∈ u₂ → x = a
⊢ a :: u₂ = u₂ ++ [a]
rw [(@eq_replicate _ a (length u₂ + 1) (a :: u₂)).2,
      (@eq_replicate _ a (length u₂ + 1) (u₂ ++ [a])).2] <;>
    constructor <;>
  simp [iff_true_intro this, or_comm]
no goals
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁✝ l₂ : List α
p✝ : l₁✝ ~ l₂
s₂✝ : Sorted r l₂
a : α
l₁ : List α
h₁ : ∀ (a' : α), a' ∈ l₁ → r a a'
s₁ : Pairwise r l₁
IH : ∀ {l₂ : List α}, l₁ ~ l₂ → Sorted r l₂ → l₁ = l₂
u₂ v₂ : List α
p : a :: l₁ ~ u₂ ++ a :: v₂
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
p' : l₁ ~ u₂ ++ v₂
⊢ u₂ ++ v₂ <+ u₂ ++ a :: v₂
simp
no goals
α : Type uu
r : α → α → Prop
a✝ : α
l : List α
inst✝ : IsAntisymm α r
l₁ l₂ : List α
p✝ : l₁ ~ l₂
s₂✝ : Sorted r l₂
a : α
u₂ v₂ : List α
s₂ : Sorted r (u₂ ++ a :: v₂)
this : a ∈ u₂ ++ a :: v₂
h₁ : ∀ (a' : α), a' ∈ u₂ ++ v₂ → r a a'
s₁ : Pairwise r (u₂ ++ v₂)
IH : ∀ {l₂ : List α}, u₂ ++ v₂ ~ l₂ → Sorted r l₂ → u₂ ++ v₂ = l₂
p : a :: (u₂ ++ v₂) ~ u₂ ++ a :: v₂
p' : u₂ ++ v₂ ~ u₂ ++ v₂
x : α
m : x ∈ u₂
⊢ x ∈ u₂ ++ v₂
simp [m]