α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h : Nodup l
this : Pairwise (fun x x_1 => x ≠ x_1) (sublists' l)
⊢ Nodup (sublistsLen n l)
α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h : Nodup l
⊢ Nodup (sublistsLen n l)
have : Pairwise (. ≠ .) l.sublists' := Pairwise.imp
  (fun h => Lex.to_ne (by convert h using 3; simp [swap, eq_comm])) h.sublists'
no goals
α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h : Nodup l
this : Pairwise (fun x x_1 => x ≠ x_1) (sublists' l)
⊢ Nodup (sublistsLen n l)
exact this.sublist (sublistsLen_sublist_sublists' _ _)
case h.e'_2.h.e'_4.h.h
α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h✝ : Nodup l
a✝ b✝ : List α
h : Lex (swap fun x x_1 => x ≠ x_1) a✝ b✝
x✝ : α
⊢ (fun x => ¬x = x✝) = fun x => x✝ ≠ x
α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h✝ : Nodup l
a✝ b✝ : List α
h : Lex (swap fun x x_1 => x ≠ x_1) a✝ b✝
⊢ Lex (fun x x_1 => x ≠ x_1) a✝ b✝
convert h using 3
no goals
case h.e'_2.h.e'_4.h.h
α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h✝ : Nodup l
a✝ b✝ : List α
h : Lex (swap fun x x_1 => x ≠ x_1) a✝ b✝
x✝ : α
⊢ (fun x => ¬x = x✝) = fun x => x✝ ≠ x
simp [swap, eq_comm]