[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ dedup l
⊢ ¬∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b
[PROOFSTEP]
simpa only [forall_mem_ne, not_not] using h
[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ dedup l
⊢ ∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b
[PROOFSTEP]
simpa only [forall_mem_ne] using h
[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ a ∈ dedup l ↔ a ∈ l
[PROOFSTEP]
have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
[GOAL]
case refine_2
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x x_1 => x ≠ x_1) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ dedup l ↔ a ∈ l
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
[PROOFSTEP]
simpa only [dedup, forall_mem_ne, not_not] using this
[GOAL]
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, (fun x x_1 => x ≠ x_1) x z → (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
[PROOFSTEP]
intros x y z xz
[GOAL]
case refine_1
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
xz : x ≠ z
⊢ (fun x x_1 => x ≠ x_1) x y ∨ (fun x x_1 => x ≠ x_1) y z
[PROOFSTEP]
exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ headI (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then headI (dedup (tail (a :: l))) else headI (a :: l)
[PROOFSTEP]
by_cases ha : a ∈ l
[GOAL]
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ headI (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then headI (dedup (tail (a :: l))) else headI (a :: l)
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ headI (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then headI (dedup (tail (a :: l))) else headI (a :: l)
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ tail (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then tail (dedup (tail (a :: l))) else dedup (tail (a :: l))
[PROOFSTEP]
by_cases ha : a ∈ l
[GOAL]
case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ tail (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then tail (dedup (tail (a :: l))) else dedup (tail (a :: l))
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ tail (dedup (a :: l)) = if headI (a :: l) ∈ tail (a :: l) then tail (dedup (tail (a :: l))) else dedup (tail (a :: l))
[PROOFSTEP]
simp [ha, List.dedup_cons_of_mem]
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
⊢ dedup l = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
⊢ a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
[PROOFSTEP]
refine' ⟨mem_dedup.1 (h.symm ▸ mem_cons_self _ _), fun ha => _, by rw [h, tail_cons]⟩
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
⊢ tail (dedup l) = l'
[PROOFSTEP]
rw [h, tail_cons]
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
ha : a ∈ l'
⊢ False
[PROOFSTEP]
have : count a l.dedup ≤ 1 := nodup_iff_count_le_one.1 (nodup_dedup l) a
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
ha : a ∈ l'
this : count a (dedup l) ≤ 1
⊢ False
[PROOFSTEP]
rw [h, count_cons_self, add_le_iff_nonpos_left] at this
[GOAL]
case refine'_1
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : dedup l = a :: l'
ha : a ∈ l'
this : count a l' ≤ 0
⊢ False
[PROOFSTEP]
exact not_le_of_lt (count_pos.2 ha) this
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
⊢ dedup l = a :: l'
[PROOFSTEP]
have := @List.cons_head!_tail α ⟨a⟩ _ (ne_nil_of_mem (mem_dedup.2 h.1))
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
this : head! (dedup l) :: tail (dedup l) = dedup l
⊢ dedup l = a :: l'
[PROOFSTEP]
have hal : a ∈ l.dedup := mem_dedup.2 h.1
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
this : head! (dedup l) :: tail (dedup l) = dedup l
hal : a ∈ dedup l
⊢ dedup l = a :: l'
[PROOFSTEP]
rw [← this, mem_cons, or_iff_not_imp_right] at hal
[GOAL]
case refine'_2
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : a ∈ l ∧ ¬a ∈ l' ∧ tail (dedup l) = l'
this : head! (dedup l) :: tail (dedup l) = dedup l
hal : ¬a ∈ tail (dedup l) → a = head! (dedup l)
⊢ dedup l = a :: l'
[PROOFSTEP]
exact this ▸ h.2.2.symm ▸ cons_eq_cons.2 ⟨(hal (h.2.2.symm ▸ h.2.1)).symm, rfl⟩
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
⊢ dedup l = [] ↔ l = []
[PROOFSTEP]
induction' l with a l hl
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
⊢ dedup [] = [] ↔ [] = []
[PROOFSTEP]
exact Iff.rfl
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
hl : dedup l = [] ↔ l = []
⊢ dedup (a :: l) = [] ↔ a :: l = []
[PROOFSTEP]
by_cases h : a ∈ l
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
hl : dedup l = [] ↔ l = []
h : a ∈ l
⊢ dedup (a :: l) = [] ↔ a :: l = []
[PROOFSTEP]
simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
hl : dedup l = [] ↔ l = []
h : ¬a ∈ l
⊢ dedup (a :: l) = [] ↔ a :: l = []
[PROOFSTEP]
simp only [List.dedup_cons_of_not_mem h, List.cons_ne_nil]
[GOAL]
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
[PROOFSTEP]
induction' l₁ with a l₁ IH
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
⊢ dedup ([] ++ l₂) = [] ∪ dedup l₂
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: l₁ ++ l₂) = a :: l₁ ∪ dedup l₂
[PROOFSTEP]
simp only [cons_union] at *
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: l₁ ++ l₂) = List.insert a (l₁ ∪ dedup l₂)
[PROOFSTEP]
rw [← IH, cons_append]
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
[PROOFSTEP]
by_cases h : a ∈ dedup (l₁ ++ l₂)
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
h : a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
[PROOFSTEP]
rw [dedup_cons_of_mem' h, insert_of_mem h]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂
h : ¬a ∈ dedup (l₁ ++ l₂)
⊢ dedup (a :: (l₁ ++ l₂)) = List.insert a (dedup (l₁ ++ l₂))
[PROOFSTEP]
rw [dedup_cons_of_not_mem' h, insert_of_not_mem h]
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ dedup (replicate (n + 2) x) = [x]
[PROOFSTEP]
rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩), replicate_dedup n.succ_ne_zero]
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a (dedup l) = if a ∈ l then 1 else 0
[PROOFSTEP]
simp_rw [count_eq_of_nodup <| nodup_dedup l, mem_dedup]
[GOAL]
α : Type u
inst✝ : DecidableEq α
p : α → Bool
l : List α
⊢ sum (map (fun x => count x l) (filter p (dedup l))) = countp p l
[PROOFSTEP]
induction' l with a as h
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
p : α → Bool
⊢ sum (map (fun x => count x []) (filter p (dedup []))) = countp p []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun x => count x (a :: as)) (filter p (dedup (a :: as)))) = countp p (a :: as)
[PROOFSTEP]
simp_rw [List.countp_cons, List.count_cons', List.sum_map_add]
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) +
      sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) =
    countp p as + if p a = true then 1 else 0
[PROOFSTEP]
congr 1
[GOAL]
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = countp p as
[PROOFSTEP]
refine' _root_.trans _ h
[GOAL]
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
[PROOFSTEP]
by_cases ha : a ∈ as
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : a ∈ as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
[PROOFSTEP]
simp [dedup_cons_of_mem ha]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum (map (fun i => count i as) (filter p (dedup (a :: as)))) = sum (map (fun x => count x as) (filter p (dedup as)))
[PROOFSTEP]
simp only [dedup_cons_of_not_mem ha, List.filter]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match p a with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
[PROOFSTEP]
match p a with
| true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
| false => simp only
[GOAL]
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match true with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
[PROOFSTEP]
simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
[GOAL]
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
ha : ¬a ∈ as
⊢ sum
      (map (fun i => count i as)
        (match false with
        | true => a :: filter p (dedup as)
        | false => filter p (dedup as))) =
    sum (map (fun i => count i as) (filter p (dedup as)))
[PROOFSTEP]
simp only
[GOAL]
case cons.e_a
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
[PROOFSTEP]
by_cases hp : p a
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
[PROOFSTEP]
refine' _root_.trans (sum_map_eq_nsmul_single a _ fun _ h _ => by simp [h]) _
[GOAL]
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h✝ : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
x✝¹ : α
h : x✝¹ ≠ a
x✝ : x✝¹ ∈ filter p (dedup (a :: as))
⊢ (if x✝¹ = a then 1 else 0) = 0
[PROOFSTEP]
simp [h]
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : p a = true
⊢ (count a (filter p (dedup (a :: as))) • if a = a then 1 else 0) = if p a = true then 1 else 0
[PROOFSTEP]
simp [hp, count_dedup]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
⊢ sum (map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))) = if p a = true then 1 else 0
[PROOFSTEP]
refine' _root_.trans (List.sum_eq_zero fun n hn => _) (by simp [hp])
[GOAL]
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
⊢ 0 = if p a = true then 1 else 0
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
⊢ n = 0
[PROOFSTEP]
obtain ⟨a', ha'⟩ := List.mem_map.1 hn
[GOAL]
case neg.intro
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha' : a' ∈ filter p (dedup (a :: as)) ∧ (if a' = a then 1 else 0) = n
⊢ n = 0
[PROOFSTEP]
split_ifs at ha'  with ha
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha : a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 1 = n
⊢ n = 0
[PROOFSTEP]
simp only [ha, mem_filter, mem_dedup, find?, mem_cons, true_or, hp, and_false, false_and] at ha'
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : sum (map (fun x => count x as) (filter p (dedup as))) = countp p as
hp : ¬p a = true
n : ℕ
hn : n ∈ map (fun i => if i = a then 1 else 0) (filter p (dedup (a :: as)))
a' : α
ha : ¬a' = a
ha' : a' ∈ filter p (dedup (a :: as)) ∧ 0 = n
⊢ n = 0
[PROOFSTEP]
exact ha'.2.symm
[GOAL]
α : Type u
inst✝ : DecidableEq α
l : List α
⊢ sum (map (fun x => count x l) (dedup l)) = length l
[PROOFSTEP]
simpa using sum_map_count_dedup_filter_eq_countp (fun _ => True) l


[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
⊢ ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ =
      Array.toList
        (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))
[PROOFSTEP]
intro r₁ r₂
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ =
    Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))
[PROOFSTEP]
rw [sublists'Aux, Array.foldl_eq_foldl_data]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁ r₂ : List (List α)
⊢ foldl (fun r l => r ++ [a :: l]) r₂ r₁ =
    Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁).data)
[PROOFSTEP]
have := List.foldl_hom Array.toList (fun r l => r.push (a :: l)) (fun r l => r ++ [a :: l]) r₁ r₂.toArray (by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁ r₂ : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α),
    (fun r l => r ++ [a :: l]) (Array.toList x) y = Array.toList ((fun r l => Array.push r (a :: l)) x y)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁ r₂ : List (List α)
this :
  foldl (fun r l => r ++ [a :: l]) (Array.toList (toArray r₂)) r₁ =
    Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) r₁)
⊢ foldl (fun r l => r ++ [a :: l]) r₂ r₁ =
    Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁).data)
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l
[PROOFSTEP]
simp only [sublists', sublists'Aux_eq_array_foldl]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ Array.toList
      (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
[PROOFSTEP]
rw [← List.foldr_hom Array.toList]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ foldr ?g₂ (Array.toList #[[]]) l =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
      [[]] l
[PROOFSTEP]
rfl
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    Array.toList
        (Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
          (Array.size (toArray (Array.toList y)))) =
      Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
[PROOFSTEP]
intros _ _
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ Array.toList
      (Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
        (Array.size (toArray (Array.toList y✝)))) =
    Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝))
[PROOFSTEP]
congr
[GOAL]
case H.e_as.h.e_4.h
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ toArray (Array.toList y✝) = y✝
[PROOFSTEP]
simp
[GOAL]
case H.e_as.h.e_5.h
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ toArray (Array.toList y✝) = y✝
[PROOFSTEP]
simp
[GOAL]
case H.e_as.h.e_7.e_a
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ toArray (Array.toList y✝) = y✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁ x✝ : List (List α)
⊢ sublists'Aux a [] x✝ = x✝ ++ map (cons a) []
[PROOFSTEP]
simp [sublists'Aux]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])
[PROOFSTEP]
rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =
    sublists'Aux a r₁ r₂ ++ [a :: l]
[PROOFSTEP]
simp [sublists'Aux]
  -- Porting note: simp can prove `sublists'_singleton`
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)
[PROOFSTEP]
simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
s t : List α
⊢ s ∈ sublists' t ↔ s <+ t
[PROOFSTEP]
induction' t with a t IH generalizing s
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
s✝ s : List α
⊢ s ∈ sublists' [] ↔ s <+ []
[PROOFSTEP]
simp only [sublists'_nil, mem_singleton]
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
s✝ s : List α
⊢ s = [] ↔ s <+ []
[PROOFSTEP]
exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
s✝ s : List α
h : s = []
⊢ s <+ []
[PROOFSTEP]
rw [h]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ s ∈ sublists' (a :: t) ↔ s <+ a :: t
[PROOFSTEP]
simp only [sublists'_cons, mem_append, IH, mem_map]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t
[PROOFSTEP]
intro h
[GOAL]
case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
⊢ s <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s
[PROOFSTEP]
intro h
[GOAL]
case cons.mp
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t
case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
[PROOFSTEP]
rcases h with (h | ⟨s, h, rfl⟩)
[GOAL]
case cons.mp.inl
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t
[PROOFSTEP]
exact sublist_cons_of_sublist _ h
[GOAL]
case cons.mp.inr.intro.intro
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t
[PROOFSTEP]
exact h.cons_cons _
[GOAL]
case cons.mpr
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
[PROOFSTEP]
cases' h with _ _ _ h s _ _ h
[GOAL]
case cons.mpr.cons
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
[PROOFSTEP]
exact Or.inl h
[GOAL]
case cons.mpr.cons₂
α : Type u
β : Type v
γ : Type w
s✝ : List α
a : α
t : List α
IH : ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s
[PROOFSTEP]
exact Or.inr ⟨s, h, rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ length (sublists' (a :: l)) = 2 ^ length (a :: l)
[PROOFSTEP]
simp_arith only [sublists'_cons, length_append, length_sublists' l, length_map, length, Nat.pow_succ', mul_succ,
  mul_zero, zero_add]
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ sublistsAux = fun a r =>
    Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))
[PROOFSTEP]
funext a r
[GOAL]
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ sublistsAux a r =
    Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))
[PROOFSTEP]
simp only [sublistsAux, Array.foldl_eq_foldl_data, Array.mkEmpty]
[GOAL]
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
[PROOFSTEP]
have :=
  foldl_hom Array.toList (fun r l => (r.push l).push (a :: l)) (fun (r : List (List α)) l => r ++ [l, a :: l]) r #[]
    (by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α),
    (fun r l => r ++ [l, a :: l]) (Array.toList x) y =
      Array.toList ((fun r l => Array.push (Array.push r l) (a :: l)) x y)
[PROOFSTEP]
simp
[GOAL]
case h.h
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
this :
  foldl (fun r l => r ++ [l, a :: l]) (Array.toList #[]) r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] r)
⊢ foldl (fun r l => r ++ [l, a :: l]) [] r =
    Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
[PROOFSTEP]
simpa using this
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ sublistsAux a [] = List.bind [] fun l => [l, a :: l]
[PROOFSTEP]
simp [sublistsAux]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = List.bind r fun l => [l, a :: l]
⊢ sublistsAux a (r ++ [l]) = List.bind (r ++ [l]) fun l => [l, a :: l]
[PROOFSTEP]
rw [append_bind, ← ih, bind_singleton, sublistsAux, foldl_append]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = List.bind r fun l => [l, a :: l]
⊢ foldl (fun r l => r ++ [l, a :: l]) (foldl (fun r l => r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
[PROOFSTEP]
simp [sublistsAux]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists l = foldr sublistsAux [[]] l
[PROOFSTEP]
simp only [sublists, sublistsAux_eq_array_foldl, Array.foldr_eq_foldr_data]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ Array.toList
      (foldr
        (fun a arr =>
          Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) (Array.mkEmpty (Array.size arr * 2)) arr 0
            (Array.size arr))
        #[[]] l) =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
      [[]] l
[PROOFSTEP]
rw [← foldr_hom Array.toList]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ foldr ?g₂ (Array.toList #[[]]) l =
    foldr
      (fun a r =>
        Array.toList
          (Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
      [[]] l
[PROOFSTEP]
rfl
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    Array.toList
        (Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) #[] (toArray (Array.toList y)) 0
          (Array.size (toArray (Array.toList y)))) =
      Array.toList
        (Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
          (Array.size y))
[PROOFSTEP]
intros _ _
[GOAL]
case H
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) #[] (toArray (Array.toList y✝)) 0
        (Array.size (toArray (Array.toList y✝)))) =
    Array.toList
      (Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) (Array.mkEmpty (Array.size y✝ * 2)) y✝ 0
        (Array.size y✝))
[PROOFSTEP]
congr
[GOAL]
case H.e_as.h.e_5.h
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ toArray (Array.toList y✝) = y✝
[PROOFSTEP]
simp
[GOAL]
case H.e_as.h.e_7.e_a
α : Type u
β : Type v
γ : Type w
l : List α
x✝ : α
y✝ : Array (List α)
⊢ toArray (Array.toList y✝) = y✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
⊢ sublists (l₁ ++ l₂) = do
    let x ← sublists l₂
    map (fun x_1 => x_1 ++ x) (sublists l₁)
[PROOFSTEP]
simp only [sublists_eq_sublistsAux, foldr_append, sublistsAux_eq_bind]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)
[PROOFSTEP]
induction l₁
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
l₂ : List α
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] [])
[PROOFSTEP]
case nil => simp
[GOAL]
α : Type u
β : Type v
γ : Type w
l₂ : List α
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] [])
[PROOFSTEP]
case nil => simp
[GOAL]
α : Type u
β : Type v
γ : Type w
l₂ : List α
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] [])
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
l₂ : List α
head✝ : α
tail✝ : List α
tail_ih✝ :
  foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
      tail✝ =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] tail✝)
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
      (head✝ :: tail✝) =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (head✝ :: tail✝))
[PROOFSTEP]
case cons a l₁ ih =>
  rw [foldr_cons, ih]
  simp [List.bind, join_join, Function.comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
      (a :: l₁) =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))
[PROOFSTEP]
case cons a l₁ ih =>
  rw [foldr_cons, ih]
  simp [List.bind, join_join, Function.comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)
⊢ foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
      (a :: l₁) =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))
[PROOFSTEP]
rw [foldr_cons, ih]
[GOAL]
α : Type u
β : Type v
γ : Type w
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)
⊢ (List.bind
      (do
        let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
        map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁))
      fun l => [l, a :: l]) =
    do
    let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))
[PROOFSTEP]
simp [List.bind, join_join, Function.comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists ([a] ++ l) = do
    let x ← sublists l
    [x, a :: x]
[PROOFSTEP]
rw [sublists_append]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ (do
      let x ← sublists l
      map (fun x_1 => x_1 ++ x) (sublists [a])) =
    do
    let x ← sublists l
    [x, a :: x]
[PROOFSTEP]
simp only [sublists_singleton, map_cons, bind_eq_bind, nil_append, cons_append, map_nil]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
a : α
⊢ sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)
[PROOFSTEP]
rw [sublists_append, sublists_singleton, bind_eq_bind, cons_bind, cons_bind, nil_bind, map_id' append_nil, append_nil]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists (reverse l) = map reverse (sublists' l)
[PROOFSTEP]
induction' l with hd tl ih <;> [rfl;
  simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton, map_eq_map,
    bind_eq_bind, map_map, cons_bind, append_nil, nil_bind, (· ∘ ·)]]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists (reverse l) = map reverse (sublists' l)
[PROOFSTEP]
induction' l with hd tl ih
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
⊢ sublists (reverse []) = map reverse (sublists' [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
hd : α
tl : List α
ih : sublists (reverse tl) = map reverse (sublists' tl)
⊢ sublists (reverse (hd :: tl)) = map reverse (sublists' (hd :: tl))
[PROOFSTEP]
simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton, map_eq_map, bind_eq_bind,
  map_map, cons_bind, append_nil, nil_bind, (· ∘ ·)]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists l = map reverse (sublists' (reverse l))
[PROOFSTEP]
rw [← sublists_reverse, reverse_reverse]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists' (reverse l) = map reverse (sublists l)
[PROOFSTEP]
simp only [sublists_eq_sublists', map_map, map_id' reverse_reverse, Function.comp]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists' l = map reverse (sublists (reverse l))
[PROOFSTEP]
rw [← sublists'_reverse, reverse_reverse]
[GOAL]
α : Type u
β : Type v
γ : Type w
s t : List α
⊢ s ∈ sublists t ↔ s <+ t
[PROOFSTEP]
rw [← reverse_sublist, ← mem_sublists', sublists'_reverse, mem_map_of_injective reverse_injective]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ length (sublists l) = 2 ^ length l
[PROOFSTEP]
simp only [sublists_eq_sublists', length_map, length_sublists', length_reverse]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ map List.ret l <+ sublists l
[PROOFSTEP]
induction' l using reverseRecOn with l a ih
[GOAL]
case H0
α : Type u
β : Type v
γ : Type w
⊢ map List.ret [] <+ sublists []
[PROOFSTEP]
simp only [map, map_append, sublists_concat]
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l : List α
a : α
ih : map List.ret l <+ sublists l
⊢ map List.ret (l ++ [a]) <+ sublists (l ++ [a])
[PROOFSTEP]
simp only [map, map_append, sublists_concat]
[GOAL]
case H0
α : Type u
β : Type v
γ : Type w
⊢ [] <+ sublists []
[PROOFSTEP]
simp only [sublists_nil, sublist_cons]
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l : List α
a : α
ih : map List.ret l <+ sublists l
⊢ map List.ret l ++ [List.ret a] <+ sublists l ++ map (fun x => x ++ [a]) (sublists l)
[PROOFSTEP]
exact
  ((append_sublist_append_left _).2 <|
        singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
    ((append_sublist_append_right _).2 ih)
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
a : α
ih : map List.ret l <+ sublists l
⊢ [] ++ [a] = List.ret a
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s
[PROOFSTEP]
unfold sublistsLenAux
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s
[PROOFSTEP]
unfold sublistsLenAux
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (Nat.add n 0 + 1) l (g ∘ f) (sublistsLenAux (Nat.add n 0) l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
    map g (sublistsLenAux (Nat.add n 0 + 1) l f (sublistsLenAux (Nat.add n 0) l (f ∘ cons a) r)) ++ s
[PROOFSTEP]
simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl, sublistsLenAux_append, sublistsLenAux_append]
[GOAL]
α✝ : Type u
β✝ : Type v
γ✝ : Type w
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) ∘ cons a = g ∘ f ∘ cons a
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r
[PROOFSTEP]
rw [sublistsLen, ← sublistsLenAux_append]
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
α : Type u_1
β : Type u_2
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l : List α
f : List α → β
r : List β
⊢ sublistsLenAux 0 l f r = f [] :: r
[PROOFSTEP]
cases l
[GOAL]
case nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
f : List α → β
r : List β
⊢ sublistsLenAux 0 [] f r = f [] :: r
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
f : List α → β
r : List β
head✝ : α
tail✝ : List α
⊢ sublistsLenAux 0 (head✝ :: tail✝) f r = f [] :: r
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
[PROOFSTEP]
rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id, append_nil]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l : List α
⊢ length (sublistsLen 0 l) = Nat.choose (length l) 0
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n✝ : ℕ
⊢ length (sublistsLen (n✝ + 1) []) = Nat.choose (length []) (n✝ + 1)
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l : List α
⊢ length (sublistsLen (n + 1) (a :: l)) = Nat.choose (length (a :: l)) (n + 1)
[PROOFSTEP]
rw [sublistsLen_succ_cons, length_append, length_sublistsLen (n + 1) l, length_map, length_sublistsLen n l, length_cons,
  Nat.choose_succ_succ, add_comm]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l : List α
⊢ sublistsLen 0 l <+ sublists' l
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) <+ sublists' (a :: l)
[PROOFSTEP]
rw [sublistsLen_succ_cons, sublists'_cons]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ sublists' l ++ map (cons a) (sublists' l)
[PROOFSTEP]
exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂
[PROOFSTEP]
induction' n with n IHn generalizing l₁ l₂
[GOAL]
case zero
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h✝ : l₁✝ <+ l₂✝
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen zero l₁ <+ sublistsLen zero l₂
[PROOFSTEP]
simp
[GOAL]
case succ
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h✝ : l₁✝ <+ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
[PROOFSTEP]
induction' h with l₁ l₂ a _ IH l₁ l₂ a s IH
[GOAL]
case succ.slnil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝ l₂✝ : List α
h : l₁✝ <+ l₂✝
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (succ n) [] <+ sublistsLen (succ n) []
[PROOFSTEP]
rfl
[GOAL]
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₁ <+ sublistsLen (succ n) (a :: l₂)
[PROOFSTEP]
refine' IH.trans _
[GOAL]
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₂ <+ sublistsLen (succ n) (a :: l₂)
[PROOFSTEP]
rw [sublistsLen_succ_cons]
[GOAL]
case succ.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
a✝ : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) l₂ <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)
[PROOFSTEP]
apply sublist_append_left
[GOAL]
case succ.cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (succ n) (a :: l₁) <+ sublistsLen (succ n) (a :: l₂)
[PROOFSTEP]
simp [sublistsLen_succ_cons]
[GOAL]
case succ.cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l₁✝¹ l₂✝¹ : List α
h : l₁✝¹ <+ l₂✝¹
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁✝ l₂✝ l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : sublistsLen (succ n) l₁ <+ sublistsLen (succ n) l₂
⊢ sublistsLen (n + 1) l₁ ++ map (cons a) (sublistsLen n l₁) <+ sublistsLen (n + 1) l₂ ++ map (cons a) (sublistsLen n l₂)
[PROOFSTEP]
exact IH.append ((IHn s).map _)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
h : l' ∈ sublistsLen 0 l
⊢ length l' = 0
[PROOFSTEP]
simp_all
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ length l' = n + 1
[PROOFSTEP]
rw [sublistsLen_succ_cons, mem_append, mem_map] at h
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ length l' = n + 1
[PROOFSTEP]
rcases h with (h | ⟨l', h, rfl⟩)
[GOAL]
case inl
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ length l' = n + 1
[PROOFSTEP]
exact length_of_sublistsLen h
[GOAL]
case inr.intro.intro
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ length (a :: l') = n + 1
[PROOFSTEP]
exact congr_arg (· + 1) (length_of_sublistsLen h)
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
h : l' <+ l
⊢ l' ∈ sublistsLen (length l') l
[PROOFSTEP]
induction' h with l₁ l₂ a s IH l₁ l₂ a s IH
[GOAL]
case slnil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' : List α
⊢ [] ∈ sublistsLen (length []) []
[PROOFSTEP]
simp
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ l₁ ∈ sublistsLen (length l₁) (a :: l₂)
[PROOFSTEP]
cases' l₁ with b l₁
[GOAL]
case cons.nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen (length []) l₂
⊢ [] ∈ sublistsLen (length []) (a :: l₂)
[PROOFSTEP]
simp
[GOAL]
case cons.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (length (b :: l₁)) l₂
⊢ b :: l₁ ∈ sublistsLen (length (b :: l₁)) (a :: l₂)
[PROOFSTEP]
rw [length, sublistsLen_succ_cons]
[GOAL]
case cons.cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (length (b :: l₁)) l₂
⊢ b :: l₁ ∈ sublistsLen (length l₁ + 1) l₂ ++ map (cons a) (sublistsLen (length l₁) l₂)
[PROOFSTEP]
exact mem_append_left _ IH
[GOAL]
case cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ a :: l₁ ∈ sublistsLen (length (a :: l₁)) (a :: l₂)
[PROOFSTEP]
rw [length, sublistsLen_succ_cons]
[GOAL]
case cons₂
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen (length l₁) l₂
⊢ a :: l₁ ∈ sublistsLen (length l₁ + 1) l₂ ++ map (cons a) (sublistsLen (length l₁) l₂)
[PROOFSTEP]
exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublistsLen (length (a :: l)) (a :: l) = [a :: l]
[PROOFSTEP]
simp only [length, sublistsLen_succ_cons, sublistsLen_length, map, sublistsLen_of_length_lt (lt_succ_self _),
  nil_append]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (swap R)) (List.sublists' (a :: l))
[PROOFSTEP]
simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp, and_imp]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (swap R)) (List.sublists' l) ∧
    Pairwise (fun a_1 b => Lex (swap R) (a :: a_1) (a :: b)) (List.sublists' l) ∧
      ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b
[PROOFSTEP]
refine' ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, _⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b
[PROOFSTEP]
rintro l₁ sl₁ x l₂ _ rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₁ : List α
sl₁ : l₁ <+ l
l₂ : List α
a✝ : l₂ <+ l
⊢ Lex (swap R) l₁ (a :: l₂)
[PROOFSTEP]
cases' l₁ with b l₁
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (swap R) [] (a :: l₂)
[PROOFSTEP]
constructor
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (swap R) (b :: l₁) (a :: l₂)
[PROOFSTEP]
exact Lex.rel (H₁ _ <| sl₁.subset <| mem_cons_self _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
l : List α
H : Pairwise R l
⊢ Pairwise (fun l₁ l₂ => Lex R (reverse l₁) (reverse l₂)) (sublists l)
[PROOFSTEP]
have := (pairwise_reverse.2 H).sublists'
[GOAL]
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (Lex (swap fun b a => R a b)) (sublists' (reverse l))
⊢ Pairwise (fun l₁ l₂ => Lex R (reverse l₁) (reverse l₂)) (sublists l)
[PROOFSTEP]
rwa [sublists'_reverse, pairwise_map] at this
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
h✝ : Nodup l
l₁ l₂ : List α
h : Lex (fun x x_1 => x ≠ x_1) (reverse l₁) (reverse l₂)
⊢ l₁ ≠ l₂
[PROOFSTEP]
simpa using h.to_ne
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ Nodup (sublists' l) ↔ Nodup l
[PROOFSTEP]
rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
[GOAL]
α : Type u
β : Type v
γ : Type w
n : ℕ
l : List α
h : Nodup l
⊢ Nodup (sublistsLen n l)
[PROOFSTEP]
have : Pairwise (· ≠ ·) l.sublists' :=
  Pairwise.imp (fun h => Lex.to_ne (by convert h using 3; simp [swap, eq_comm])) h.sublists'
[GOAL]
α : 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✝
[PROOFSTEP]
convert h using 3
[GOAL]
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
[PROOFSTEP]
simp [swap, eq_comm]
[GOAL]
α : 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)
[PROOFSTEP]
exact this.sublist (sublistsLen_sublist_sublists' _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
⊢ sublists (map f []) = map (map f) (sublists [])
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ sublists (map f (a :: l)) = map (map f) (sublists (a :: l))
[PROOFSTEP]
rw [map_cons, sublists_cons, bind_eq_bind, sublists_map f l, sublists_cons, bind_eq_bind, map_eq_bind, map_eq_bind]
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ (List.bind (List.bind (sublists l) fun x => [map f x]) fun x => [x, f a :: x]) =
    List.bind (List.bind (sublists l) fun x => [x, a :: x]) fun x => [map f x]
[PROOFSTEP]
induction sublists l
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ (List.bind (List.bind [] fun x => [map f x]) fun x => [x, f a :: x]) =
    List.bind (List.bind [] fun x => [x, a :: x]) fun x => [map f x]
[PROOFSTEP]
simp [*]
  --Porting note: new theorem
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  (List.bind (List.bind tail✝ fun x => [map f x]) fun x => [x, f a :: x]) =
    List.bind (List.bind tail✝ fun x => [x, a :: x]) fun x => [map f x]
⊢ (List.bind (List.bind (head✝ :: tail✝) fun x => [map f x]) fun x => [x, f a :: x]) =
    List.bind (List.bind (head✝ :: tail✝) fun x => [x, a :: x]) fun x => [map f x]
[PROOFSTEP]
simp [*]
  --Porting note: new theorem
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
⊢ sublists' (map f []) = map (map f) (sublists' [])
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ sublists' (map f (a :: l)) = map (map f) (sublists' (a :: l))
[PROOFSTEP]
simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]
  --Porting note: moved because it is now used to prove `sublists_cons_perm_append`
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists l ~ sublists' l
[PROOFSTEP]
rw [← finRange_map_get l, sublists_map, sublists'_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ map (map (get l)) (sublists (finRange (length l))) ~ map (map (get l)) (sublists' (finRange (length l)))
[PROOFSTEP]
refine' Perm.map _ _
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ sublists (finRange (length l)) ~ sublists' (finRange (length l))
[PROOFSTEP]
exact (perm_ext (nodup_sublists.2 (nodup_finRange _)) (nodup_sublists'.2 (nodup_finRange _))).2 (by simp)
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (a : List (Fin (length l))), a ∈ sublists (finRange (length l)) ↔ a ∈ sublists' (finRange (length l))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists' (a :: l) ~ sublists l ++ map (cons a) (sublists l)
[PROOFSTEP]
rw [sublists'_cons]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists' l ++ map (cons a) (sublists' l) ~ sublists l ++ map (cons a) (sublists l)
[PROOFSTEP]
exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ revzip (sublists l) → l₁ ++ l₂ ~ l
[PROOFSTEP]
rw [revzip]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l) (reverse (sublists l)) → l₁ ++ l₂ ~ l
[PROOFSTEP]
induction' l using List.reverseRecOn with l' a ih
[GOAL]
case H0
α : Type u
β : Type v
γ : Type w
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists []) (reverse (sublists [])) → l₁ ++ l₂ ~ []
[PROOFSTEP]
intro l₁ l₂ h
[GOAL]
case H0
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists []) (reverse (sublists []))
⊢ l₁ ++ l₂ ~ []
[PROOFSTEP]
simp at h
[GOAL]
case H0
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
[PROOFSTEP]
simp [h]
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a]))) → l₁ ++ l₂ ~ l' ++ [a]
[PROOFSTEP]
intro l₁ l₂ h
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a])))
⊢ l₁ ++ l₂ ~ l' ++ [a]
[PROOFSTEP]
rw [sublists_concat, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at * <;> [skip; simp]
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a])))
⊢ l₁ ++ l₂ ~ l' ++ [a]
[PROOFSTEP]
rw [sublists_concat, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x => x ++ [a]) (zip (sublists l') (reverse (sublists l'))) ++
      map (Prod.map (fun x => x ++ [a]) id) (zip (sublists l') (reverse (sublists l')))
⊢ l₁ ++ l₂ ~ l' ++ [a]
[PROOFSTEP]
skip
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    zip (sublists l' ++ map (fun x => x ++ [a]) (sublists l'))
      (reverse (map (fun x => x ++ [a]) (sublists l')) ++ reverse (sublists l'))
⊢ length (sublists l') = length (reverse (map (fun x => x ++ [a]) (sublists l')))
[PROOFSTEP]
simp
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x => x ++ [a]) (zip (sublists l') (reverse (sublists l'))) ++
      map (Prod.map (fun x => x ++ [a]) id) (zip (sublists l') (reverse (sublists l')))
⊢ l₁ ++ l₂ ~ l' ++ [a]
[PROOFSTEP]
simp only [Prod.mk.inj_iff, mem_map, mem_append, Prod.map_mk, Prod.exists] at h
[GOAL]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ zip (sublists l') (reverse (sublists l')) ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ a_1 b, (a_1, b) ∈ zip (sublists l') (reverse (sublists l')) ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
⊢ l₁ ++ l₂ ~ l' ++ [a]
[PROOFSTEP]
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
[GOAL]
case H1.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ zip (sublists l') (reverse (sublists l'))
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]
[PROOFSTEP]
rw [← append_assoc]
[GOAL]
case H1.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ zip (sublists l') (reverse (sublists l'))
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
[PROOFSTEP]
exact (ih _ _ h).append_right _
[GOAL]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ zip (sublists l') (reverse (sublists l'))
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]
[PROOFSTEP]
rw [append_assoc]
[GOAL]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ zip (sublists l') (reverse (sublists l'))
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
[PROOFSTEP]
apply (perm_append_comm.append_left _).trans
[GOAL]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ zip (sublists l') (reverse (sublists l'))
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]
[PROOFSTEP]
rw [← append_assoc]
[GOAL]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ zip (sublists l') (reverse (sublists l'))
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]
[PROOFSTEP]
exact (ih _ _ h).append_right _
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ revzip (sublists' l) → l₁ ++ l₂ ~ l
[PROOFSTEP]
rw [revzip]
[GOAL]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
[PROOFSTEP]
induction' l with a l IH
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' []) (reverse (sublists' [])) → l₁ ++ l₂ ~ []
[PROOFSTEP]
intro l₁ l₂ h
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' (a :: l)) (reverse (sublists' (a :: l))) → l₁ ++ l₂ ~ a :: l
[PROOFSTEP]
intro l₁ l₂ h
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' []) (reverse (sublists' []))
⊢ l₁ ++ l₂ ~ []
[PROOFSTEP]
simp at h
[GOAL]
case nil
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
[PROOFSTEP]
simp [h]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' (a :: l)) (reverse (sublists' (a :: l)))
⊢ l₁ ++ l₂ ~ a :: l
[PROOFSTEP]
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at * <;> [simp at h ; simp]
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' (a :: l)) (reverse (sublists' (a :: l)))
⊢ l₁ ++ l₂ ~ a :: l
[PROOFSTEP]
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id (cons a)) (zip (sublists' l) (reverse (sublists' l))) ++
      map (Prod.map (cons a) id) (zip (sublists' l) (reverse (sublists' l)))
⊢ l₁ ++ l₂ ~ a :: l
[PROOFSTEP]
simp at h
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    zip (sublists' l ++ map (cons a) (sublists' l)) (reverse (map (cons a) (sublists' l)) ++ reverse (sublists' l))
⊢ length (sublists' l) = length (reverse (map (cons a) (sublists' l)))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ zip (sublists' l) (reverse (sublists' l)) ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ a_1, (a_1, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) ∧ a :: a_1 = l₁
⊢ l₁ ++ l₂ ~ a :: l
[PROOFSTEP]
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
[GOAL]
case cons.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ zip (sublists' l) (reverse (sublists' l))
⊢ l₁ ++ a :: l₂' ~ a :: l
[PROOFSTEP]
exact perm_middle.trans ((IH _ _ h).cons _)
[GOAL]
case cons.inr.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ zip (sublists' l) (reverse (sublists' l))
⊢ a :: l₁' ++ l₂ ~ a :: l
[PROOFSTEP]
exact (IH _ _ h).cons _
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l : List α
⊢ (List.bind (range (length l + 1)) fun n => sublistsLen n l) ~ sublists' l
[PROOFSTEP]
induction' l with h tl l_ih
[GOAL]
case nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ (List.bind (range (length [] + 1)) fun n => sublistsLen n []) ~ sublists' []
[PROOFSTEP]
simp [range_succ]
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (List.bind (range (length (h :: tl) + 1)) fun n => sublistsLen n (h :: tl)) ~ sublists' (h :: tl)
[PROOFSTEP]
simp_rw [range_succ_eq_map, length, cons_bind, map_bind, sublistsLen_succ_cons, sublists'_cons, List.sublistsLen_zero,
  List.singleton_append]
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ ([] :: List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) ~
    sublists' tl ++ map (cons h) (sublists' tl)
[PROOFSTEP]
refine' ((bind_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans _
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ [] ::
      ((List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
        List.bind (range (length tl + 1)) fun a => map (cons h) (sublistsLen a tl)) ~
    sublists' tl ++ map (cons h) (sublists' tl)
[PROOFSTEP]
simp_rw [← List.bind_map, ← cons_append]
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ ([] :: List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
      map (cons h) (List.bind (range (length tl + 1)) fun a => sublistsLen a tl) ~
    sublists' tl ++ map (cons h) (sublists' tl)
[PROOFSTEP]
rw [← List.singleton_append, ← List.sublistsLen_zero tl]
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (sublistsLen 0 tl ++ List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
      map (cons h) (List.bind (range (length tl + 1)) fun a => sublistsLen a tl) ~
    sublists' tl ++ map (cons h) (sublists' tl)
[PROOFSTEP]
refine' Perm.append _ (l_ih.map _)
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (sublistsLen 0 tl ++ List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ~ sublists' tl
[PROOFSTEP]
rw [List.range_succ, append_bind, bind_singleton, sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil, ←
  List.map_bind (fun n => sublistsLen n tl) Nat.succ, ← cons_bind 0 _ fun n => sublistsLen n tl, ← range_succ_eq_map]
[GOAL]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
[PROOFSTEP]
exact l_ih


[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂
[PROOFSTEP]
cases' h with _ _ _ _ _ h _ _ _ _ h
[GOAL]
case cons
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂
case rel α : Type u r : α → α → Prop inst✝ : IsIrrefl α r a : α l₁ l₂ : List α h : r a a ⊢ Lex r l₁ l₂
[PROOFSTEP]
exacts [h, (irrefl_of r a h).elim]
[GOAL]
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
[PROOFSTEP]
rcases trichotomous_of r a b with (ab | rfl | ab)
[GOAL]
case inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
[PROOFSTEP]
exact Or.inl (rel ab)
[GOAL]
case inr.inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)
[PROOFSTEP]
exact (aux _ l₂ _ h).imp cons cons
[GOAL]
case inr.inr
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
[PROOFSTEP]
exact Or.inr (rel ab)
[GOAL]
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
[PROOFSTEP]
rcases trichotomous_of r a b with (ab | rfl | ab)
[GOAL]
case inl
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ : List α
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
[PROOFSTEP]
exact Or.inl (rel ab)
[GOAL]
case inr.inl
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ l₂ : List α
⊢ Lex r (a :: l₁) (a :: l₂) ∨ a :: l₁ = a :: l₂ ∨ Lex r (a :: l₂) (a :: l₁)
[PROOFSTEP]
exact (aux l₁ l₂).imp cons (Or.imp (congr_arg _) cons)
[GOAL]
case inr.inr
α : Type u
r : α → α → Prop
inst✝ : IsTrichotomous α r
a : α
l₁ : List α
b : α
l₂ : List α
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ a :: l₁ = b :: l₂ ∨ Lex r (b :: l₂) (a :: l₁)
[PROOFSTEP]
exact Or.inr (Or.inr (rel ab))
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
l₁ : List α
h : Lex r l₁ []
⊢ False
[PROOFSTEP]
cases h
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
[PROOFSTEP]
haveI := decidableRel r l₁ l₂
[GOAL]
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
[PROOFSTEP]
refine' decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ Lex r (a :: l₁) (b :: l₂)
[PROOFSTEP]
rcases h with (h | ⟨rfl, h⟩)
[GOAL]
case refine'_1.inl
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ Lex r (a :: l₁) (b :: l₂)
[PROOFSTEP]
exact Lex.rel h
[GOAL]
case refine'_1.inr.intro
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ Lex r (a :: l₁) (a :: l₂)
[PROOFSTEP]
exact Lex.cons h
[GOAL]
case refine'_2
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
[PROOFSTEP]
rcases h with (_ | h | h)
[GOAL]
case refine'_2.cons
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂
[PROOFSTEP]
exact Or.inr ⟨rfl, h⟩
[GOAL]
case refine'_2.rel
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
[PROOFSTEP]
exact Or.inl h
[GOAL]
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : length l₁ ≤ length l₂
h : l₁ ≠ l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂
[PROOFSTEP]
induction' l₁ with a l₁ IH generalizing l₂
[GOAL]
case nil
α : Type u
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : length l₁ ≤ length l₂✝
h✝ : l₁ ≠ l₂✝
l₂ : List α
H : length [] ≤ length l₂
h : [] ≠ l₂
⊢ Lex (fun x x_1 => x ≠ x_1) [] l₂
[PROOFSTEP]
cases' l₂ with b l₂
[GOAL]
case cons
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
l₂ : List α
H : length (a :: l₁) ≤ length l₂
h : a :: l₁ ≠ l₂
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) l₂
[PROOFSTEP]
cases' l₂ with b l₂
[GOAL]
case nil.nil
α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H✝ : length l₁ ≤ length l₂
h✝ : l₁ ≠ l₂
H : length [] ≤ length []
h : [] ≠ []
⊢ Lex (fun x x_1 => x ≠ x_1) [] []
[PROOFSTEP]
contradiction
[GOAL]
case nil.cons
α : Type u
inst✝ : DecidableEq α
l₁ l₂✝ : List α
H✝ : length l₁ ≤ length l₂✝
h✝ : l₁ ≠ l₂✝
b : α
l₂ : List α
H : length [] ≤ length (b :: l₂)
h : [] ≠ b :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) [] (b :: l₂)
[PROOFSTEP]
apply nil
[GOAL]
case cons.nil
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂ : List α
H✝ : length l₁✝ ≤ length l₂
h✝ : l₁✝ ≠ l₂
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
H : length (a :: l₁) ≤ length []
h : a :: l₁ ≠ []
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) []
[PROOFSTEP]
exact (not_lt_of_ge H).elim (succ_pos _)
[GOAL]
case cons.cons
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
b : α
l₂ : List α
H : length (a :: l₁) ≤ length (b :: l₂)
h : a :: l₁ ≠ b :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (b :: l₂)
[PROOFSTEP]
by_cases ab : a = b
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
b : α
l₂ : List α
H : length (a :: l₁) ≤ length (b :: l₂)
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (b :: l₂)
[PROOFSTEP]
subst b
[GOAL]
case pos
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
l₂ : List α
H : length (a :: l₁) ≤ length (a :: l₂)
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (a :: l₂)
[PROOFSTEP]
apply cons
[GOAL]
case pos.h
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
l₂ : List α
H : length (a :: l₁) ≤ length (a :: l₂)
h : a :: l₁ ≠ a :: l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂
[PROOFSTEP]
exact IH (le_of_succ_le_succ H) (mt (congr_arg _) h)
[GOAL]
case neg
α : Type u
inst✝ : DecidableEq α
l₁✝ l₂✝ : List α
H✝ : length l₁✝ ≤ length l₂✝
h✝ : l₁✝ ≠ l₂✝
a : α
l₁ : List α
IH : ∀ {l₂ : List α}, length l₁ ≤ length l₂ → l₁ ≠ l₂ → Lex (fun x x_1 => x ≠ x_1) l₁ l₂
b : α
l₂ : List α
H : length (a :: l₁) ≤ length (b :: l₂)
h : a :: l₁ ≠ b :: l₂
ab : ¬a = b
⊢ Lex (fun x x_1 => x ≠ x_1) (a :: l₁) (b :: l₂)
[PROOFSTEP]
exact rel ab
[GOAL]
α : Type u
l₁ l₂ : List α
H : length l₁ ≤ length l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
[PROOFSTEP]
classical exact Decidable.List.Lex.ne_iff H
[GOAL]
α : Type u
l₁ l₂ : List α
H : length l₁ ≤ length l₂
⊢ Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
[PROOFSTEP]
exact Decidable.List.Lex.ne_iff H
[GOAL]
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ lt l l' ↔ Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ lt l l' → Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
⊢ Lex (fun x x_1 => x < x_1) l l' → lt l l'
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : lt l l'
⊢ Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
induction h with
| nil b bs => exact Lex.nil
| @head a as b bs hab => apply Lex.rel; assumption
|
  @tail a as b bs hab hba _ ih =>
  have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
  subst b; apply Lex.cons; assumption
[GOAL]
case mp
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : lt l l'
⊢ Lex (fun x x_1 => x < x_1) l l'
[PROOFSTEP]
induction h with
| nil b bs => exact Lex.nil
| @head a as b bs hab => apply Lex.rel; assumption
|
  @tail a as b bs hab hba _ ih =>
  have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
  subst b; apply Lex.cons; assumption
[GOAL]
case mp.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
b : α
bs : List α
⊢ Lex (fun x x_1 => x < x_1) [] (b :: bs)
[PROOFSTEP]

| nil b bs => exact Lex.nil
[GOAL]
case mp.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
b : α
bs : List α
⊢ Lex (fun x x_1 => x < x_1) [] (b :: bs)
[PROOFSTEP]
exact Lex.nil
[GOAL]
case mp.head
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
[PROOFSTEP]

| @head a as b bs hab => apply Lex.rel; assumption
[GOAL]
case mp.head
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
[PROOFSTEP]
apply Lex.rel
[GOAL]
case mp.head.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : a < b
⊢ a < b
[PROOFSTEP]
assumption
[GOAL]
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : ¬a < b
hba : ¬b < a
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
[PROOFSTEP]

|
  @tail a as b bs hab hba _ ih =>
  have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
  subst b; apply Lex.cons; assumption
[GOAL]
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : ¬a < b
hba : ¬b < a
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
[PROOFSTEP]
have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab)
[GOAL]
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
hab : ¬a < b
hba : ¬b < a
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
heq : a = b
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (b :: bs)
[PROOFSTEP]
subst b
[GOAL]
case mp.tail
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
hab hba : ¬a < a
⊢ Lex (fun x x_1 => x < x_1) (a :: as) (a :: bs)
[PROOFSTEP]
apply Lex.cons
[GOAL]
case mp.tail.h
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
a✝ : lt as bs
ih : Lex (fun x x_1 => x < x_1) as bs
hab hba : ¬a < a
⊢ Lex (fun x x_1 => x < x_1) as bs
[PROOFSTEP]
assumption
[GOAL]
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : Lex (fun x x_1 => x < x_1) l l'
⊢ lt l l'
[PROOFSTEP]
induction h with
| @nil a as => apply lt.nil
| @cons a as bs _ ih => apply lt.tail <;> simp [ih]
| @rel a as b bs h => apply lt.head; assumption
[GOAL]
case mpr
α : Type u
inst✝ : LinearOrder α
l l' : List α
h : Lex (fun x x_1 => x < x_1) l l'
⊢ lt l l'
[PROOFSTEP]
induction h with
| @nil a as => apply lt.nil
| @cons a as bs _ ih => apply lt.tail <;> simp [ih]
| @rel a as b bs h => apply lt.head; assumption
[GOAL]
case mpr.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
⊢ lt [] (a :: as)
[PROOFSTEP]

| @nil a as => apply lt.nil
[GOAL]
case mpr.nil
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
⊢ lt [] (a :: as)
[PROOFSTEP]
apply lt.nil
[GOAL]
case mpr.cons
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
h✝ : Lex (fun x x_1 => x < x_1) as bs
ih : lt as bs
⊢ lt (a :: as) (a :: bs)
[PROOFSTEP]

| @cons a as bs _ ih => apply lt.tail <;> simp [ih]
[GOAL]
case mpr.cons
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
h✝ : Lex (fun x x_1 => x < x_1) as bs
ih : lt as bs
⊢ lt (a :: as) (a :: bs)
[PROOFSTEP]
apply lt.tail
[GOAL]
case mpr.cons.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
h✝ : Lex (fun x x_1 => x < x_1) as bs
ih : lt as bs
⊢ ¬a < a
[PROOFSTEP]
simp [ih]
[GOAL]
case mpr.cons.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
h✝ : Lex (fun x x_1 => x < x_1) as bs
ih : lt as bs
⊢ ¬a < a
[PROOFSTEP]
simp [ih]
[GOAL]
case mpr.cons.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as bs : List α
h✝ : Lex (fun x x_1 => x < x_1) as bs
ih : lt as bs
⊢ lt as bs
[PROOFSTEP]
simp [ih]
[GOAL]
case mpr.rel
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ lt (a :: as) (b :: bs)
[PROOFSTEP]

| @rel a as b bs h => apply lt.head; assumption
[GOAL]
case mpr.rel
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ lt (a :: as) (b :: bs)
[PROOFSTEP]
apply lt.head
[GOAL]
case mpr.rel.a
α : Type u
inst✝ : LinearOrder α
l l' : List α
a : α
as : List α
b : α
bs : List α
h : a < b
⊢ a < b
[PROOFSTEP]
assumption