case slnil
α : Type uu
β : Type vv
l₁✝¹ l₂✝ l₁✝ l₂ l : List α
d✝ : Nodup l
s₁✝ : l₁✝ <+ l
h✝ : l₁✝ ~ l₂
l₁ : List α
d : Nodup []
s₁ : l₁ <+ []
h : l₁ ~ []
⊢ l₁ = []

case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
d : Nodup (a :: l)
s₁ : l₁ <+ a :: l
h : l₁ ~ l₂
⊢ l₁ = l₂

case cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
d : Nodup (a :: l)
s₁ : l₁ <+ a :: l
h : l₁ ~ a :: l₂
⊢ l₁ = a :: l₂
α : Type uu
β : Type vv
l₁✝ l₂✝ l₁ l₂ l : List α
d : Nodup l
s₁ : l₁ <+ l
s₂ : l₂ <+ l
h : l₁ ~ l₂
⊢ l₁ = l₂
induction' s₂ with l₂ l a s₂ IH l₂ l a _ IH generalizing l₁
no goals
case slnil
α : Type uu
β : Type vv
l₁✝¹ l₂✝ l₁✝ l₂ l : List α
d✝ : Nodup l
s₁✝ : l₁✝ <+ l
h✝ : l₁✝ ~ l₂
l₁ : List α
d : Nodup []
s₁ : l₁ <+ []
h : l₁ ~ []
⊢ l₁ = []
exact h.eq_nil
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
s₁ : l₁ <+ a :: l
h : l₁ ~ l₂
d : ¬a ∈ l ∧ Nodup l
⊢ l₁ = l₂
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
d : Nodup (a :: l)
s₁ : l₁ <+ a :: l
h : l₁ ~ l₂
⊢ l₁ = l₂
simp at d
case cons.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
h : l₁ ~ l₂
d : ¬a ∈ l ∧ Nodup l
s₁ : l₁ <+ l
⊢ l₁ = l₂

case cons.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
d : ¬a ∈ l ∧ Nodup l
l₁ : List α
h : a :: l₁ ~ l₂
s₁ : l₁ <+ l
⊢ a :: l₁ = l₂
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
s₁ : l₁ <+ a :: l
h : l₁ ~ l₂
d : ¬a ∈ l ∧ Nodup l
⊢ l₁ = l₂
cases' s₁ with _ _ _ s₁ l₁ _ _ s₁
no goals
case cons.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
h : l₁ ~ l₂
d : ¬a ∈ l ∧ Nodup l
s₁ : l₁ <+ l
⊢ l₁ = l₂
exact IH d.2 s₁ h
case cons.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
d : ¬a ∈ l ∧ Nodup l
l₁ : List α
h : a :: l₁ ~ l₂
s₁ : l₁ <+ l
⊢ a ∈ l
case cons.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
d : ¬a ∈ l ∧ Nodup l
l₁ : List α
h : a :: l₁ ~ l₂
s₁ : l₁ <+ l
⊢ a :: l₁ = l₂
apply d.1.elim
no goals
case cons.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
s₂ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
d : ¬a ∈ l ∧ Nodup l
l₁ : List α
h : a :: l₁ ~ l₂
s₁ : l₁ <+ l
⊢ a ∈ l
exact Subperm.subset ⟨_, h.symm, s₂⟩ (mem_cons_self _ _)
case cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
s₁ : l₁ <+ a :: l
h : l₁ ~ a :: l₂
d : ¬a ∈ l ∧ Nodup l
⊢ l₁ = a :: l₂
case cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
d : Nodup (a :: l)
s₁ : l₁ <+ a :: l
h : l₁ ~ a :: l₂
⊢ l₁ = a :: l₂
simp at d
case cons₂.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
h : l₁ ~ a :: l₂
d : ¬a ∈ l ∧ Nodup l
s₁ : l₁ <+ l
⊢ l₁ = a :: l₂

case cons₂.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
d : ¬a ∈ l ∧ Nodup l
l₁ : List α
h : a :: l₁ ~ a :: l₂
s₁ : l₁ <+ l
⊢ a :: l₁ = a :: l₂
case cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
s₁ : l₁ <+ a :: l
h : l₁ ~ a :: l₂
d : ¬a ∈ l ∧ Nodup l
⊢ l₁ = a :: l₂
cases' s₁ with _ _ _ s₁ l₁ _ _ s₁
case cons₂.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
h : l₁ ~ a :: l₂
d : ¬a ∈ l ∧ Nodup l
s₁ : l₁ <+ l
⊢ a ∈ l
case cons₂.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
h : l₁ ~ a :: l₂
d : ¬a ∈ l ∧ Nodup l
s₁ : l₁ <+ l
⊢ l₁ = a :: l₂
apply d.1.elim
no goals
case cons₂.cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
l₁ : List α
h : l₁ ~ a :: l₂
d : ¬a ∈ l ∧ Nodup l
s₁ : l₁ <+ l
⊢ a ∈ l
exact Subperm.subset ⟨_, h, s₁⟩ (mem_cons_self _ _)
no goals
case cons₂.cons₂
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ l₁✝ l₂✝ l✝ : List α
d✝ : Nodup l✝
s₁✝ : l₁✝ <+ l✝
h✝ : l₁✝ ~ l₂✝
l₂ l : List α
a : α
a✝ : l₂ <+ l
IH : ∀ {l₁ : List α}, Nodup l → l₁ <+ l → l₁ ~ l₂ → l₁ = l₂
d : ¬a ∈ l ∧ Nodup l
l₁ : List α
h : a :: l₁ ~ a :: l₂
s₁ : l₁ <+ l
⊢ a :: l₁ = a :: l₂
rw [IH d.2 s₁ h.cons_inv]
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ l₁ l₂ l : List α
d : Nodup l
s₁ : l₁ <+ l
s₂ : l₂ <+ l
h : l₁ = l₂
⊢ l₁ ~ l₂
rw [h]