case intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ l₂
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ a :: l₁ <+~ l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ l₂
s : l₁ <+~ l₂
⊢ a :: l₁ <+~ l₂
rcases s with ⟨l, p, s⟩
case intro.intro.slnil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ []
p : [] ~ l₁
⊢ a :: l₁ <+~ []

case intro.intro.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝

case intro.intro.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : a✝¹ :: l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝
case intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ l₂
l : List α
p : l ~ l₁
s : l <+ l₂
⊢ a :: l₁ <+~ l₂
induction s generalizing l₁
case intro.intro.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝

case intro.intro.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : a✝¹ :: l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝
case intro.intro.slnil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ []
p : [] ~ l₁
⊢ a :: l₁ <+~ []

case intro.intro.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝

case intro.intro.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : a✝¹ :: l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝
case slnil => cases h₂
no goals
case intro.intro.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
a : α
l₂ l l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
a_ih✝ : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ l₂✝ → l₁✝ ~ l₁ → a :: l₁ <+~ l₂✝
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ a✝¹ :: l₂✝
p : a✝¹ :: l₁✝ ~ l₁
⊢ a :: l₁ <+~ a✝¹ :: l₂✝
case cons₂ r₁ r₂ b _ ih =>
  have bm : b ∈ l₁ := p.subset <| mem_cons_self _ _
  have am : a ∈ r₂ := by
    simp only [find?, mem_cons] at h₂
    exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm
  rcases mem_split bm with ⟨t₁, t₂, rfl⟩
  have st : t₁ ++ t₂ <+ t₁ ++ b :: t₂ := by simp
  rcases ih (d₁.sublist st) (mt (fun x => st.subset x) h₁) am
      (Perm.cons_inv <| p.trans perm_middle) with
    ⟨t, p', s'⟩
  exact
    ⟨b :: t, (p'.cons b).trans <| (swap _ _ _).trans (perm_middle.symm.cons a), s'.cons₂ _⟩
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ []
p : [] ~ l₁
⊢ a :: l₁ <+~ []
cases h₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : r₁ ~ l₁
⊢ a :: l₁ <+~ b :: r₂
simp at h₂
case inl
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
e : a = b
⊢ a :: l₁ <+~ b :: r₂

case inr
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
m : a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
h₂ : a = b ∨ a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂
cases' h₂ with e m
case inl
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
⊢ a :: l₁ <+~ a :: r₂
case inl
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
e : a = b
⊢ a :: l₁ <+~ b :: r₂
subst b
no goals
case inl
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
⊢ a :: l₁ <+~ a :: r₂
exact ⟨a :: r₁, p.cons a, s'.cons₂ _⟩
case inr.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s'✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
m : a ∈ r₂
t : List α
p' : t ~ a :: l₁
s' : t <+ r₂
⊢ a :: l₁ <+~ b :: r₂
case inr
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s' : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
m : a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂
rcases ih d₁ h₁ m p with ⟨t, p', s'⟩
no goals
case inr.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
s'✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : r₁ ~ l₁
m : a ∈ r₂
t : List α
p' : t ~ a :: l₁
s' : t <+ r₂
⊢ a :: l₁ <+~ b :: r₂
exact ⟨t, p', s'.cons _⟩
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: r₁ ~ l₁
bm : b ∈ l₁
⊢ a :: l₁ <+~ b :: r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: r₁ ~ l₁
⊢ a :: l₁ <+~ b :: r₂
have bm : b ∈ l₁ := p.subset <| mem_cons_self _ _
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: r₁ ~ l₁
bm : b ∈ l₁
am : a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: r₁ ~ l₁
bm : b ∈ l₁
⊢ a :: l₁ <+~ b :: r₂
have am : a ∈ r₂ := by
  simp only [find?, mem_cons] at h₂
  exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm
case intro.intro
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: r₁ ~ l₁
bm : b ∈ l₁
am : a ∈ r₂
⊢ a :: l₁ <+~ b :: r₂
rcases mem_split bm with ⟨t₁, t₂, rfl⟩
case intro.intro
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
st : t₁ ++ t₂ <+ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂
case intro.intro
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂
have st : t₁ ++ t₂ <+ t₁ ++ b :: t₂ := by simp
case intro.intro.intro.intro
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
st : t₁ ++ t₂ <+ t₁ ++ b :: t₂
t : List α
p' : t ~ a :: (t₁ ++ t₂)
s' : t <+ r₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂
case intro.intro
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
st : t₁ ++ t₂ <+ t₁ ++ b :: t₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂
rcases ih (d₁.sublist st) (mt (fun x => st.subset x) h₁) am
    (Perm.cons_inv <| p.trans perm_middle) with
  ⟨t, p', s'⟩
no goals
case intro.intro.intro.intro
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
st : t₁ ++ t₂ <+ t₁ ++ b :: t₂
t : List α
p' : t ~ a :: (t₁ ++ t₂)
s' : t <+ r₂
⊢ a :: (t₁ ++ b :: t₂) <+~ b :: r₂
exact
  ⟨b :: t, (p'.cons b).trans <| (swap _ _ _).trans (perm_middle.symm.cons a), s'.cons₂ _⟩
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : b :: r₁ ~ l₁
bm : b ∈ l₁
h₂ : a = b ∨ a ∈ r₂
⊢ a ∈ r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
h₂ : a ∈ b :: r₂
p : b :: r₁ ~ l₁
bm : b ∈ l₁
⊢ a ∈ r₂
simp only [find?, mem_cons] at h₂
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
l₁ : List α
d₁ : Nodup l₁
h₁ : ¬a ∈ l₁
p : b :: r₁ ~ l₁
bm : b ∈ l₁
h₂ : a = b ∨ a ∈ r₂
⊢ a ∈ r₂
exact h₂.resolve_left fun e => h₁ <| e.symm ▸ bm
no goals
α : Type uu
β : Type vv
l₁ l₂✝ : List α
a : α
l₂ l r₁ r₂ : List α
b : α
a✝ : r₁ <+ r₂
ih : ∀ {l₁ : List α}, Nodup l₁ → ¬a ∈ l₁ → a ∈ r₂ → r₁ ~ l₁ → a :: l₁ <+~ r₂
h₂ : a ∈ b :: r₂
am : a ∈ r₂
t₁ t₂ : List α
d₁ : Nodup (t₁ ++ b :: t₂)
h₁ : ¬a ∈ t₁ ++ b :: t₂
p : b :: r₁ ~ t₁ ++ b :: t₂
bm : b ∈ t₁ ++ b :: t₂
⊢ t₁ ++ t₂ <+ t₁ ++ b :: t₂
simp