case mk.mk
α✝ : Type ?u.88487
β : Type ?u.88490
γ : Type ?u.88493
α : Type u_1
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk Setoid.r s)
h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝ } t
⊢ a ∈ disjUnion { val := Quot.mk Setoid.r s, nodup := nodup✝ } t h ↔
    a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝ } ∨ a ∈ t
α✝ : Type ?u.88487
β : Type ?u.88490
γ : Type ?u.88493
α : Type u_1
s t : Finset α
h : _root_.Disjoint s t
a : α
⊢ a ∈ disjUnion s t h ↔ a ∈ s ∨ a ∈ t
rcases s with ⟨⟨s⟩⟩
case mk.mk.mk.mk
α✝ : Type ?u.88487
β : Type ?u.88490
γ : Type ?u.88493
α : Type u_1
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk Setoid.r s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk Setoid.r t)
h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ }
⊢ a ∈ disjUnion { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } ∨ a ∈ { val := Quot.mk Setoid.r t, nodup := nodup✝ }
case mk.mk
α✝ : Type ?u.88487
β : Type ?u.88490
γ : Type ?u.88493
α : Type u_1
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk Setoid.r s)
h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝ } t
⊢ a ∈ disjUnion { val := Quot.mk Setoid.r s, nodup := nodup✝ } t h ↔
    a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝ } ∨ a ∈ t
rcases t with ⟨⟨t⟩⟩
no goals
case mk.mk.mk.mk
α✝ : Type ?u.88487
β : Type ?u.88490
γ : Type ?u.88493
α : Type u_1
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk Setoid.r s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk Setoid.r t)
h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ }
⊢ a ∈ disjUnion { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } ∨ a ∈ { val := Quot.mk Setoid.r t, nodup := nodup✝ }
apply List.mem_append