Theorem: List.foldl_product (LeanColls/MathlibUpstream.lean)

State before:
γ : Type u_1
α : Type u_2
β : Type u_3
L1 : List α
L2 : List β
f : γ → α × β → γ
init : γ
⊢ foldl f init (L1 ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init L1
Tactic:
induction L1 generalizing init <;> simp
State after:
case cons
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (init : γ), foldl f init (tail✝ ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tail✝
init : γ
⊢ foldl f (foldl f init (map (fun b => (head✝, b)) L2)) (tail✝ ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (head✝, b)) init L2) tail✝

State before:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl f (foldl f init (map (fun b => (hd, b)) L2)) (tl ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Tactic:
case cons hd tl ih =>
rw [ih]; simp [foldl_map]
State after:
no goals

State before:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl f (foldl f init (map (fun b => (hd, b)) L2)) (tl ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Tactic:
rw [ih]
State after:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl f init (map (fun b => (hd, b)) L2)) tl =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl

State before:
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl f init (map (fun b => (hd, b)) L2)) tl =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
Tactic:
simp [foldl_map]
State after:
no goals