case nil
ι : Type ?u.234160
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α β : Type u
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
a : α
⊢ foldl f' (g a) (map g []) = g (foldl f a [])

case cons
ι : Type ?u.234160
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α β : Type u
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (a : α), foldl f' (g a) (map g tail✝) = g (foldl f a tail✝)
a : α
⊢ foldl f' (g a) (map g (head✝ :: tail✝)) = g (foldl f a (head✝ :: tail✝))
ι : Type ?u.234160
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α β : Type u
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : List α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldl f' (g a) (map g l) = g (foldl f a l)
induction l generalizing a
no goals
case nil
ι : Type ?u.234160
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α β : Type u
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
a : α
⊢ foldl f' (g a) (map g []) = g (foldl f a [])
simp
no goals
case cons
ι : Type ?u.234160
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α β : Type u
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (a : α), foldl f' (g a) (map g tail✝) = g (foldl f a tail✝)
a : α
⊢ foldl f' (g a) (map g (head✝ :: tail✝)) = g (foldl f a (head✝ :: tail✝))
simp [*, h]