[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ s t x : Multiset α
⊢ x ∈ (fun s t => Finset.map (Equiv.toEmbedding equivDFinsupp.symm) (Finset.Icc (↑toDFinsupp s) (↑toDFinsupp t))) s t ↔
    s ≤ x ∧ x ≤ t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.map (Equiv.toEmbedding equivDFinsupp.symm) (Finset.Icc (↑toDFinsupp (s ⊓ t)) (↑toDFinsupp (s ⊔ t))) =
    Finset.map (Equiv.toEmbedding equivDFinsupp.symm) (uIcc (↑toDFinsupp s) (↑toDFinsupp t))
[PROOFSTEP]
simp [uIcc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Icc s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s)
[PROOFSTEP]
simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply, toDFinsupp_support]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Ico s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Ioc s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Ioo s t) = ∏ i in toFinset s ∪ toFinset t, (count i t + 1 - count i s) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (uIcc s t) = ∏ i in toFinset s ∪ toFinset t, (Int.natAbs (↑(count i t) - ↑(count i s)) + 1)
[PROOFSTEP]
simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply, toDFinsupp_support]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.card (Finset.Iic s) = ∏ i in toFinset s, (count i s + 1)
[PROOFSTEP]
simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]
