case h
α✝ : Type ?u.35910
β : Type ?u.35913
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s
α✝ : Type ?u.35910
β : Type ?u.35913
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
n : ℕ
s : Sym α n
⊢ map id s = s
ext
case h
α✝ : Type ?u.35910
β : Type ?u.35913
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
n : ℕ
s : Sym α n
⊢ { val := ↑s, property := (_ : (fun s => ↑Multiset.card s = n) ↑s) } = s
case h
α✝ : Type ?u.35910
β : Type ?u.35913
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s
simp [Sym.map]
no goals
case h
α✝ : Type ?u.35910
β : Type ?u.35913
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a b : α✝
α : Type u_1
n : ℕ
s : Sym α n
⊢ { val := ↑s, property := (_ : (fun s => ↑Multiset.card s = n) ↑s) } = s
rfl