ι : Type ?u.133759
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
⊢ join (map (List.ret ∘ f) l) = map f l
ι : Type ?u.133759
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
⊢ List.bind l (List.ret ∘ f) = map f l
unfold List.bind
case cons
ι : Type ?u.133759
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : join (map ((fun a => [a]) ∘ f) tail✝) = map f tail✝
⊢ join (map ((fun a => [a]) ∘ f) tail✝) = map f tail✝
ι : Type ?u.133759
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
⊢ join (map (List.ret ∘ f) l) = map f l
induction l <;> simp [map, join, List.ret, cons_append, nil_append, *] at *
no goals
case cons
ι : Type ?u.133759
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : join (map ((fun a => [a]) ∘ f) tail✝) = map f tail✝
⊢ join (map ((fun a => [a]) ∘ f) tail✝) = map f tail✝
assumption