case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
H : [] ⊆ l₂
⊢ [] <+~ l₂

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
a : α
l₁' : List α
h : ∀ (a' : α), a' ∈ l₁' → a ≠ a'
d : Pairwise (fun x x_1 => x ≠ x_1) l₁'
IH : l₁' ⊆ l₂ → l₁' <+~ l₂
H : a :: l₁' ⊆ l₂
⊢ a :: l₁' <+~ l₂
α : Type uu
β : Type vv
l₁ l₂ : List α
d : Nodup l₁
H : l₁ ⊆ l₂
⊢ l₁ <+~ l₂
induction' d with a l₁' h d IH
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
H : [] ⊆ l₂
⊢ [] <+~ l₂
exact ⟨nil, Perm.nil, nil_sublist _⟩
case cons.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
a : α
l₁' : List α
h : ∀ (a' : α), a' ∈ l₁' → a ≠ a'
d : Pairwise (fun x x_1 => x ≠ x_1) l₁'
IH : l₁' ⊆ l₂ → l₁' <+~ l₂
H : a :: l₁' ⊆ l₂
H₁ : a ∈ l₂
H₂ : ∀ (x : α), x ∈ l₁' → x ∈ l₂
⊢ a :: l₁' <+~ l₂
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
a : α
l₁' : List α
h : ∀ (a' : α), a' ∈ l₁' → a ≠ a'
d : Pairwise (fun x x_1 => x ≠ x_1) l₁'
IH : l₁' ⊆ l₂ → l₁' <+~ l₂
H : a :: l₁' ⊆ l₂
⊢ a :: l₁' <+~ l₂
cases' forall_mem_cons.1 H with H₁ H₂
case cons.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
a : α
l₁' : List α
d : Pairwise (fun x x_1 => x ≠ x_1) l₁'
IH : l₁' ⊆ l₂ → l₁' <+~ l₂
H : a :: l₁' ⊆ l₂
H₁ : a ∈ l₂
H₂ : ∀ (x : α), x ∈ l₁' → x ∈ l₂
h : ¬a ∈ l₁'
⊢ a :: l₁' <+~ l₂
case cons.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
a : α
l₁' : List α
h : ∀ (a' : α), a' ∈ l₁' → a ≠ a'
d : Pairwise (fun x x_1 => x ≠ x_1) l₁'
IH : l₁' ⊆ l₂ → l₁' <+~ l₂
H : a :: l₁' ⊆ l₂
H₁ : a ∈ l₂
H₂ : ∀ (x : α), x ∈ l₁' → x ∈ l₂
⊢ a :: l₁' <+~ l₂
simp at h
no goals
case cons.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
H✝ : l₁ ⊆ l₂
a : α
l₁' : List α
d : Pairwise (fun x x_1 => x ≠ x_1) l₁'
IH : l₁' ⊆ l₂ → l₁' <+~ l₂
H : a :: l₁' ⊆ l₂
H₁ : a ∈ l₂
H₂ : ∀ (x : α), x ∈ l₁' → x ∈ l₂
h : ¬a ∈ l₁'
⊢ a :: l₁' <+~ l₂
exact cons_subperm_of_mem d h H₁ (IH H₂)