case mk.mk
α✝ : Type ?u.27619
β : Type ?u.27622
n✝ n' m : ℕ
s : Sym α✝ n✝
a✝ b : α✝
α : Type u_1
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : ↑Multiset.card (Quot.mk Setoid.r l) = n
⊢ (a :: ↑symEquivSym' { val := Quot.mk Setoid.r l, property := property✝ }) =
    ↑symEquivSym' (a ::ₛ { val := Quot.mk Setoid.r l, property := property✝ })
α✝ : Type ?u.27619
β : Type ?u.27622
n✝ n' m : ℕ
s✝ : Sym α✝ n✝
a✝ b : α✝
α : Type u_1
n : ℕ
a : α
s : Sym α n
⊢ (a :: ↑symEquivSym' s) = ↑symEquivSym' (a ::ₛ s)
rcases s with ⟨⟨l⟩, _⟩
no goals
case mk.mk
α✝ : Type ?u.27619
β : Type ?u.27622
n✝ n' m : ℕ
s : Sym α✝ n✝
a✝ b : α✝
α : Type u_1
n : ℕ
a : α
val✝ : Multiset α
l : List α
property✝ : ↑Multiset.card (Quot.mk Setoid.r l) = n
⊢ (a :: ↑symEquivSym' { val := Quot.mk Setoid.r l, property := property✝ }) =
    ↑symEquivSym' (a ::ₛ { val := Quot.mk Setoid.r l, property := property✝ })
rfl