-- Mathlib/MeasureTheory/PiSystem.lean
theorem mem_generatePiSystem_iUnion_elim {α β} {g : β → Set (Set α)} (h_pi : ∀ b, IsPiSystem (g b))
    (t : Set α) (h_t : t ∈ generatePiSystem (⋃ b, g b)) :
    ∃ (T : Finset β) (f : β → Set α), (t = ⋂ b ∈ T, f b) ∧ ∀ b ∈ T, f b ∈ g b

Proof state:
case h.left.h
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
⊢ (∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)) ↔
    ∀ (i : β),
      (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
        (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)

Tactic:
constructor <;> intro h1 b <;> by_cases hbs : b ∈ T_s <;> by_cases hbt : b ∈ T_t' <;>
    specialize h1 b <;>
  simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff] at h1 ⊢

Result:
case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_s b ∧ a ∈ f_t' b
⊢ a ∈ f_s b ∩ f_t' b

case neg
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
b : β
hbs : b ∈ T_s
hbt : b ∉ T_t'
h1 : a ∈ f_s b ∧ True
⊢ a ∈ f_s b ∧ True

case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
b : β
hbs : b ∉ T_s
hbt : b ∈ T_t'
h1 : True ∧ a ∈ f_t' b
⊢ True ∧ a ∈ f_t' b

case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_s b ∩ f_t' b
⊢ a ∈ f_s b ∧ a ∈ f_t' b

case neg
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
b : β
hbs : b ∈ T_s
hbt : b ∉ T_t'
h1 : a ∈ f_s b ∧ True
⊢ a ∈ f_s b ∧ True

case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
a : α
b : β
hbs : b ∉ T_s
hbt : b ∈ T_t'
h1 : True ∧ a ∈ f_t' b
⊢ True ∧ a ∈ f_t' b

Proof state:
case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ f_s b ∩ f_t' b ∈ g b

Tactic:
refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)

Result:
case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ⊆ f_s b ∩ f_t' b

Proof state:
case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∉ T_s
hbt : b ∈ T_t'
⊢ f_t' b ∈ g b

Tactic:
exact h_t' b hbt

Result:
no goals