α : Type uu
β : Type vv
l₁ l₂ s : List α
hs : Nodup s
⊢ Nodup (permutations' s)
α : Type uu
β : Type vv
l₁ l₂ s : List α
hs : Nodup s
⊢ Nodup (permutations s)
rw [(permutations_perm_permutations' s).nodup_iff]
case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
⊢ Nodup (permutations' [])

case cons
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ Nodup (permutations' (x :: l))
α : Type uu
β : Type vv
l₁ l₂ s : List α
hs : Nodup s
⊢ Nodup (permutations' s)
induction' hs with x l h h' IH
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
⊢ Nodup (permutations' [])
simp
case cons
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ Nodup (List.bind (permutations' l) (permutations'Aux x))
case cons
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ Nodup (permutations' (x :: l))
rw [permutations']
case cons
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ (∀ (x_1 : List α), x_1 ∈ permutations' l → Nodup (permutations'Aux x x_1)) ∧
    Pairwise (fun a b => Disjoint (permutations'Aux x a) (permutations'Aux x b)) (permutations' l)
case cons
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ Nodup (List.bind (permutations' l) (permutations'Aux x))
rw [nodup_bind]
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ ∀ (x_1 : List α), x_1 ∈ permutations' l → Nodup (permutations'Aux x x_1)

case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ Pairwise (fun a b => Disjoint (permutations'Aux x a) (permutations'Aux x b)) (permutations' l)
case cons
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ (∀ (x_1 : List α), x_1 ∈ permutations' l → Nodup (permutations'Aux x x_1)) ∧
    Pairwise (fun a b => Disjoint (permutations'Aux x a) (permutations'Aux x b)) (permutations' l)
constructor
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
ys : List α
hy : ys ∈ permutations' l
⊢ Nodup (permutations'Aux x ys)
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ ∀ (x_1 : List α), x_1 ∈ permutations' l → Nodup (permutations'Aux x x_1)
intro ys hy
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
ys : List α
hy : ys ~ l
⊢ Nodup (permutations'Aux x ys)
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
ys : List α
hy : ys ∈ permutations' l
⊢ Nodup (permutations'Aux x ys)
rw [mem_permutations'] at hy
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
ys : List α
hy : ys ~ l
⊢ ¬x ∈ l
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
ys : List α
hy : ys ~ l
⊢ Nodup (permutations'Aux x ys)
rw [nodup_permutations'Aux_iff, hy.mem_iff]
no goals
case cons.left
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
ys : List α
hy : ys ~ l
⊢ ¬x ∈ l
exact fun H => h x H rfl
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
⊢ Disjoint (permutations'Aux x as) (permutations'Aux x bs)
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
⊢ Pairwise (fun a b => Disjoint (permutations'Aux x a) (permutations'Aux x b)) (permutations' l)
refine' IH.pairwise_of_forall_ne fun as ha bs hb H => _
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
⊢ ∀ (a : List α), a ∈ permutations'Aux x as → ∀ (b : List α), b ∈ permutations'Aux x bs → a ≠ b
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
⊢ Disjoint (permutations'Aux x as) (permutations'Aux x bs)
rw [disjoint_iff_ne]
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
⊢ False
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
⊢ ∀ (a : List α), a ∈ permutations'Aux x as → ∀ (b : List α), b ∈ permutations'Aux x bs → a ≠ b
rintro a ha' b hb' rfl
case cons.right.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
⊢ False
case cons.right
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
⊢ False
obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
m : ℕ
hm : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm } = a
⊢ False
case cons.right.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
⊢ False
obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
m : ℕ
hm : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm } = a
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ∈ permutations' l
bs : List α
hb : bs ∈ permutations' l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
m : ℕ
hm : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm } = a
⊢ False
rw [mem_permutations'] at ha hb
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
m : ℕ
hm : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm } = a
hl : length as = length bs
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
m : ℕ
hm : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm } = a
⊢ False
have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn✝ } = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm✝ } = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn } = a
m : ℕ
hm : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm } = a
hl : length as = length bs
⊢ False
simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : get (permutations'Aux x as) { val := n, isLt := hn✝ } = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : get (permutations'Aux x bs) { val := m, isLt := hm✝ } = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
⊢ False
rw [← nthLe, nthLe_permutations'Aux] at hn' hm'
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
⊢ False
have hx :
  nthLe (insertNth n x as) m (by rwa [length_insertNth _ _ hn, Nat.lt_succ_iff, hl]) = x :=
  by simp [hn', ← hm', hm]
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
⊢ False
have hx' :
  nthLe (insertNth m x bs) n (by rwa [length_insertNth _ _ hm, Nat.lt_succ_iff, ← hl]) =
    x :=
  by simp [hm', ← hn', hn]
case cons.right.intro.mk.intro.mk.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
⊢ False

case cons.right.intro.mk.intro.mk.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n = m
⊢ False

case cons.right.intro.mk.intro.mk.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
⊢ False
case cons.right.intro.mk.intro.mk
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
⊢ False
rcases lt_trichotomy n m with (ht | ht | ht)
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
⊢ m < length (insertNth n x as)
rwa [length_insertNth _ _ hn, Nat.lt_succ_iff, hl]
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
⊢ nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
simp [hn', ← hm', hm]
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
⊢ n < length (insertNth m x bs)
rwa [length_insertNth _ _ hm, Nat.lt_succ_iff, ← hl]
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
⊢ nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
simp [hm', ← hn', hn]
case cons.right.intro.mk.intro.mk.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
⊢ x ∈ bs
case cons.right.intro.mk.intro.mk.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
⊢ False
suffices x ∈ bs by exact h x (hb.subset this) rfl
case cons.right.intro.mk.intro.mk.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
⊢ nthLe bs n (_ : n < length bs) ∈ bs
case cons.right.intro.mk.intro.mk.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
⊢ x ∈ bs
rw [← hx', nthLe_insertNth_of_lt _ _ _ _ ht (ht.trans_le hm)]
no goals
case cons.right.intro.mk.intro.mk.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
⊢ nthLe bs n (_ : n < length bs) ∈ bs
exact nthLe_mem _ _ _
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n < m
this : x ∈ bs
⊢ False
exact h x (hb.subset this) rfl
case cons.right.intro.mk.intro.mk.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n = m
hn' : insertNth m x as = a
⊢ False
case cons.right.intro.mk.intro.mk.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n = m
⊢ False
simp only [ht] at hm' hn'
case cons.right.intro.mk.intro.mk.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n = m
hn' : insertNth m x as = insertNth m x bs
⊢ False
case cons.right.intro.mk.intro.mk.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n = m
hn' : insertNth m x as = a
⊢ False
rw [← hm'] at hn'
no goals
case cons.right.intro.mk.intro.mk.inr.inl
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : n = m
hn' : insertNth m x as = insertNth m x bs
⊢ False
exact H (insertNth_injective _ _ hn')
case cons.right.intro.mk.intro.mk.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
⊢ x ∈ as
case cons.right.intro.mk.intro.mk.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
⊢ False
suffices x ∈ as by exact h x (ha.subset this) rfl
case cons.right.intro.mk.intro.mk.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
⊢ nthLe as m (_ : m < length as) ∈ as
case cons.right.intro.mk.intro.mk.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
⊢ x ∈ as
rw [← hx, nthLe_insertNth_of_lt _ _ _ _ ht (ht.trans_le hn)]
no goals
case cons.right.intro.mk.intro.mk.inr.inr
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
⊢ nthLe as m (_ : m < length as) ∈ as
exact nthLe_mem _ _ _
no goals
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun x x_1 => x ≠ x_1) l
IH : Nodup (permutations' l)
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn✝ : n < length (permutations'Aux x as)
hn' : insertNth n x as = a
m : ℕ
hm✝ : m < length (permutations'Aux x bs)
hm' : insertNth m x bs = a
hl : length as = length bs
hn : n ≤ length as
hm : m ≤ length bs
hx : nthLe (insertNth n x as) m (_ : m < length (insertNth n x as)) = x
hx' : nthLe (insertNth m x bs) n (_ : n < length (insertNth m x bs)) = x
ht : m < n
this : x ∈ as
⊢ False
exact h x (ha.subset this) rfl