α : 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₁)))
α : 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₁)))
intro r₁ r₂
α : 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)
α : 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₁)))
rw [sublists'Aux, Array.foldl_eq_foldl_data]
α : 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)
α : 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)
have := List.foldl_hom Array.toList (fun r l => r.push (a :: l))
  (fun r l => r ++ [a :: l]) r₁ r₂.toArray (by simp)
no goals
α : 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)
simpa using this
no goals
α : 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)
simp