case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ product l₁ l₂ = productTR l₁ l₂
⊢ @product = @productTR
funext α β l₁ l₂
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ (List.bind l₁ fun a => map (Prod.mk a) l₂) =
    (foldl (fun acc a => foldl (fun acc b => Array.push acc (a, b)) acc l₂) #[] l₁).data
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ product l₁ l₂ = productTR l₁ l₂
simp [product, productTR]
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ (List.bind l₁ fun a => map (Prod.mk a) l₂) = #[].data ++ List.bind l₁ ?h.h.h.h.G

case h.h.h.h.G
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ α → List (α × β)

case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α), (foldl (fun acc b => Array.push acc (a, b)) acc l₂).data = acc.data ++ ?h.h.h.h.G a
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ (List.bind l₁ fun a => map (Prod.mk a) l₂) =
    (foldl (fun acc a => foldl (fun acc b => Array.push acc (a, b)) acc l₂) #[] l₁).data
rw [Array.foldl_data_eq_bind]
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α),
    (foldl (fun acc b => Array.push acc (a, b)) acc l₂).data = acc.data ++ map (Prod.mk a) l₂
case h.h.h.h
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ (List.bind l₁ fun a => map (Prod.mk a) l₂) = #[].data ++ List.bind l₁ ?h.h.h.h.G

case h.h.h.h.G
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ α → List (α × β)

case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α), (foldl (fun acc b => Array.push acc (a, b)) acc l₂).data = acc.data ++ ?h.h.h.h.G a
rfl
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
acc✝ : Array (α × β)
a✝ : α
⊢ (foldl (fun acc b => Array.push acc (a✝, b)) acc✝ l₂).data = acc✝.data ++ map (Prod.mk a✝) l₂
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
⊢ ∀ (acc : Array (α × β)) (a : α),
    (foldl (fun acc b => Array.push acc (a, b)) acc l₂).data = acc.data ++ map (Prod.mk a) l₂
intros
no goals
case h.h.h.h.H
α : Type u_2
β : Type u_1
l₁ : List α
l₂ : List β
acc✝ : Array (α × β)
a✝ : α
⊢ (foldl (fun acc b => Array.push acc (a✝, b)) acc✝ l₂).data = acc✝.data ++ map (Prod.mk a✝) l₂
apply Array.foldl_data_eq_map