α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ insert ∅ S
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert ∅ 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 ∅ S
hst : Set.Nonempty (s ∩ t)
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ insert ∅ 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 ∅ S
hst : Set.Nonempty (s ∩ t)
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S
simp [hs]
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 = ∅
⊢ s ∩ t ∈ insert ∅ 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 ∅ S
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ 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 = ∅
⊢ s ∩ t ∈ insert ∅ S
simp [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 ∅ S
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)