α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
⊢ i ∈ t
α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
⊢ s ⊆ t
rintro i hi
case intro
α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
⊢ i ∈ t
obtain ⟨a, hai⟩ := h₁ i hi
case intro.intro.intro
α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t
case intro
α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.5199
γ : Type ?u.5202
ι : Type u_2
ι' : Type ?u.5208
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : (⋃ (i : ι) (_ : i ∈ s), f i) ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t
rwa [h₀.eq (subset_union_left _ _ hi) (subset_union_right _ _ hj)
    (not_disjoint_iff.2 ⟨a, hai, haj⟩)]