α : Type u_1
β : Type ?u.453063
γ : Type ?u.453066
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
α : Type u_1
β : Type ?u.453063
γ : Type ?u.453066
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinset s ⊂ toFinset t ↔ s ⊂ t
simp_rw [Finset.ssubset_def, toFinset_subset]
no goals
α : Type u_1
β : Type ?u.453063
γ : Type ?u.453066
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
rfl