-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_piiUnionInter (π : ι → Set (Set α)) (hpi : ∀ x, IsPiSystem (π x)) (S : Set ι) :
    IsPiSystem (piiUnionInter π S)

Proof state:
case h
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n

Tactic:
split_ifs with hn1 hn2 h

Result:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
⊢ f1 n ∩ f2 n ∈ π n

case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∉ p2
⊢ f1 n ∩ univ ∈ π n

case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n

case neg
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∉ p1
h : n ∉ p2
⊢ univ ∩ univ ∈ π n

Proof state:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ False

Tactic:
rw [h_inter_eq] at h_nonempty

Result:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : (⋂ i ∈ p1 ∪ p2, g i).Nonempty
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ False

Proof state:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : (⋂ i ∈ p1 ∪ p2, g i).Nonempty
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ ⋂ i ∈ p1 ∪ p2, g i = ∅

Tactic:
refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)

Result:
case pos
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : (⋂ i ∈ p1 ∪ p2, g i).Nonempty
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ ⋂ (_ : n ∈ p1 ∪ p2), g n ⊆ ∅