case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
⊢ a :: l ~ l₁' ++ l₂'
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
⊢ a :: l ~ l₁' ++ l₂'
cases' e : split l with l₁ l₂
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
fst_eq✝ : a :: l₂ = l₁'
snd_eq✝ : l₁ = l₂'
⊢ a :: l ~ l₁' ++ l₂'
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
⊢ a :: l ~ l₁' ++ l₂'
injection (split_cons_of_eq _ e).symm.trans h
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
⊢ a :: l ~ a :: l₂ ++ l₁
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁' l₂' : List α
h : split (a :: l) = (l₁', l₂')
l₁ l₂ : List α
e : split l = (l₁, l₂)
fst_eq✝ : a :: l₂ = l₁'
snd_eq✝ : l₁ = l₂'
⊢ a :: l ~ l₁' ++ l₂'
substs l₁' l₂'
no goals
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l l₁ l₂ : List α
e : split l = (l₁, l₂)
h : split (a :: l) = (a :: l₂, l₁)
⊢ a :: l ~ a :: l₂ ++ l₁
exact ((perm_split e).trans perm_append_comm).cons a