α : Type u
β : Type v
γ : Type w
l : List α
⊢ map (map (get l)) (sublists (finRange (length l))) ~ map (map (get l)) (sublists' (finRange (length l)))
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists l ~ sublists' l
rw [← finRange_map_get l, sublists_map, sublists'_map]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists (finRange (length l)) ~ sublists' (finRange (length l))
α : Type u
β : Type v
γ : Type w
l : List α
⊢ map (map (get l)) (sublists (finRange (length l))) ~ map (map (get l)) (sublists' (finRange (length l)))
refine' Perm.map _ _
no goals
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists (finRange (length l)) ~ sublists' (finRange (length l))
exact (perm_ext (nodup_sublists.2 (nodup_finRange _)) (nodup_sublists'.2 (nodup_finRange _))).2
  (by simp)
no goals
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (a : List (Fin (length l))), a ∈ sublists (finRange (length l)) ↔ a ∈ sublists' (finRange (length l))
simp