α✝ : Type ?u.36412
β✝ : Type ?u.36415
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s
α✝ : Type ?u.36412
β✝ : Type ?u.36415
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ ↑(map g (map f s)) = ↑(map (g ∘ f) s)
dsimp only [Sym.map]
no goals
α✝ : Type ?u.36412
β✝ : Type ?u.36415
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s
simp