α : Type u_1
β : Type u_2
γ : Type ?u.89298
dec : DecidableEq α
a b : α
f : α → β
P : RegularExpression α
⊢ 1 = map f P ^ 0
α : Type u_1
β : Type u_2
γ : Type ?u.89298
dec : DecidableEq α
a b : α
f : α → β
P : RegularExpression α
⊢ map f (P ^ 0) = map f P ^ 0
dsimp
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.89298
dec : DecidableEq α
a b : α
f : α → β
P : RegularExpression α
⊢ 1 = map f P ^ 0
rfl