case h
α : Type u_1
β : Type u_2
γ : Type ?u.114268
f : α → β
t : α
x✝ : Multiset α
⊢ (map f ∘ cons t) x✝ = (cons (f t) ∘ map f) x✝
α : Type u_1
β : Type u_2
γ : Type ?u.114268
f : α → β
t : α
⊢ map f ∘ cons t = cons (f t) ∘ map f
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.114268
f : α → β
t : α
x✝ : Multiset α
⊢ (map f ∘ cons t) x✝ = (cons (f t) ∘ map f) x✝
simp