α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ π i ⊆ piiUnionInter π S
have h_ss : {i} ⊆ S := by
  intro j hj
  rw [mem_singleton_iff] at hj
  rwa [hj]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S
refine' Subset.trans _ (piiUnionInter_mono_right h_ss)
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}
rw [piiUnionInter_singleton]
no goals
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}
exact subset_union_left _ _
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j ∈ {i}
⊢ j ∈ S
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ {i} ⊆ S
intro j hj
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j = i
⊢ j ∈ S
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j ∈ {i}
⊢ j ∈ S
rw [mem_singleton_iff] at hj
no goals
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j = i
⊢ j ∈ S
rwa [hj]