α : Type u_1
β : Type ?u.148065
γ : Type ?u.148068
ι : Sort ?u.148071
ι' : Sort ?u.148074
ι₂ : Sort ?u.148077
κ : ι → Sort ?u.148082
κ₁ : ι → Sort ?u.148087
κ₂ : ι → Sort ?u.148092
κ' : ι' → Sort ?u.148097
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S
α : Type u_1
β : Type ?u.148065
γ : Type ?u.148068
ι : Sort ?u.148071
ι' : Sort ?u.148074
ι₂ : Sort ?u.148077
κ : ι → Sort ?u.148082
κ₁ : ι → Sort ?u.148087
κ₂ : ι → Sort ?u.148092
κ' : ι' → Sort ?u.148097
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ ∅
rw [← h]
no goals
α : Type u_1
β : Type ?u.148065
γ : Type ?u.148068
ι : Sort ?u.148071
ι' : Sort ?u.148074
ι₂ : Sort ?u.148077
κ : ι → Sort ?u.148082
κ₁ : ι → Sort ?u.148087
κ₂ : ι → Sort ?u.148092
κ' : ι' → Sort ?u.148097
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S
exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)