no goals
α : Type u_1
β : Type u_3
γ : Type u_2
dec : DecidableEq α
a b : α
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R + S)) = map (g ∘ f) (R + S)
simp only [map, Function.comp_apply, map_map]
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
dec : DecidableEq α
a b : α
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R * S)) = map (g ∘ f) (R * S)
simp only [map, Function.comp_apply, map_map]
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
dec : DecidableEq α
a b : α
g : β → γ
f : α → β
R : RegularExpression α
⊢ map g (map f (star R)) = map (g ∘ f) (star R)
simp only [map, Function.comp_apply, map_map]