α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬a ∈ ⋃ (x : ι) (_ : x ∈ t), f x
α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
⊢ ((⋃ (i : ι) (_ : i ∈ s), f i) \ ⋃ (i : ι) (_ : i ∈ t), f i) = ⋃ (i : ι) (_ : i ∈ s \ t), f i
refine'
  (biUnion_diff_biUnion_subset f s t).antisymm
    (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, _⟩)
α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i j, a ∈ f i
α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬a ∈ ⋃ (x : ι) (_ : x ∈ t), f x
rw [mem_iUnion₂]
case intro.intro
α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False
α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i j, a ∈ f i
rintro ⟨j, hj, haj⟩
no goals
case intro.intro
α : Type u_2
β : Type ?u.3238
γ : Type ?u.3241
ι : Type u_1
ι' : Type ?u.3247
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False
exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩