α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ insert univ S
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert univ S)
intro s hs t ht hst
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
hs : s = univ
⊢ s ∩ t ∈ insert univ S

case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ insert univ S
cases' hs with hs hs
no goals
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
hs : s = univ
⊢ s ∩ t ∈ insert univ S
cases' ht with ht ht <;> simp [hs, ht]
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S

case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S
cases' ht with ht ht
no goals
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S
simp [hs, ht]
no goals
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)