case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ List.sigma l₁ l₂ = sigmaTR l₁ l₂
⊢ @List.sigma = @sigmaTR
funext α β l₁ l₂
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ (List.bind l₁ fun a => map (Sigma.mk a) (l₂ a)) =
    (foldl (fun acc a => foldl (fun acc b => Array.push acc { fst := a, snd := b }) acc (l₂ a)) #[] l₁).data
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ List.sigma l₁ l₂ = sigmaTR l₁ l₂
simp [List.sigma, sigmaTR]
case h.h.h.h
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ (List.bind l₁ fun a => map (Sigma.mk a) (l₂ a)) = #[].data ++ List.bind l₁ ?h.h.h.h.G

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

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

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

case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ ∀ (acc : Array ((a : α) × β a)) (a : α),
    (foldl (fun acc b => Array.push acc { fst := a, snd := b }) acc (l₂ a)).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₂ : (a : α) → List (β a)
acc✝ : Array ((a : α) × β a)
a✝ : α
⊢ (foldl (fun acc b => Array.push acc { fst := a✝, snd := b }) acc✝ (l₂ a✝)).data =
    acc✝.data ++ map (Sigma.mk a✝) (l₂ a✝)
case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
⊢ ∀ (acc : Array ((a : α) × β a)) (a : α),
    (foldl (fun acc b => Array.push acc { fst := a, snd := b }) acc (l₂ a)).data = acc.data ++ map (Sigma.mk a) (l₂ a)
intros
no goals
case h.h.h.h.H
α : Type u_2
β : α → Type u_1
l₁ : List α
l₂ : (a : α) → List (β a)
acc✝ : Array ((a : α) × β a)
a✝ : α
⊢ (foldl (fun acc b => Array.push acc { fst := a✝, snd := b }) acc✝ (l₂ a✝)).data =
    acc✝.data ++ map (Sigma.mk a✝) (l₂ a✝)
apply Array.foldl_data_eq_map