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

Proof state:
case intro.intro.intro.refine_1.h.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ b ∈ Finset.image (fun x => ↑x) T, Function.extend (fun x => ↑x) f (fun x => ∅) b → a ∈ ⋂ b ∈ T, f b

Tactic:
simp (config := { proj := false }) only
  [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]

Result:
case intro.intro.intro.refine_1.h.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
⊢ (∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨a_1, b⟩) →
    ∀ (a_2 : β) (b : s a_2), ⟨a_2, b⟩ ∈ T → a ∈ f ⟨a_2, b⟩

Proof state:
case intro.intro.intro.refine_1.h.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨a_1, b⟩
b : β
h_b : s b
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨b, h_b⟩ → a ∈ f ⟨b, h_b⟩

Tactic:
rw [Subtype.val_injective.extend_apply]

Result:
case intro.intro.intro.refine_1.h.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨a_1, b⟩
b : β
h_b : s b
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ f ⟨b, h_b⟩ → a ∈ f ⟨b, h_b⟩

Proof state:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)
⊢ t ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)

Tactic:
suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b by rwa [h1]

Result:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)
⊢ ⋃ b, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b

Proof state:
case intro.intro.intro
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∃ T_1 f_1, ↑T_1 ⊆ s ∧ ⋂ b ∈ T, f b = ⋂ b ∈ T_1, f_1 b ∧ ∀ b ∈ T_1, f_1 b ∈ g b

Tactic:
refine
  ⟨T.image (fun x : s => (x : β)),
    Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ⋂ b ∈ T, f b = ⋂ b ∈ Finset.image (fun x => ↑x) T, Function.extend (fun x => ↑x) f (fun x => ∅) b

case intro.intro.intro.refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∀ b ∈ Finset.image (fun x => ↑x) T, Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b

Proof state:
case intro.intro.intro.refine_2.intro
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : ⟨b, ⋯⟩ ∈ T
h_b_alt : b = ↑⟨b, h_b_w⟩
⊢ f ⟨b, h_b_w⟩ ∈ g ↑⟨b, h_b_w⟩

Tactic:
apply h_t'

Result:
case intro.intro.intro.refine_2.intro.a
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : ⟨b, ⋯⟩ ∈ T
h_b_alt : b = ↑⟨b, h_b_w⟩
⊢ ⟨b, h_b_w⟩ ∈ T

Proof state:
case intro.intro.intro.refine_1.h.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨a_1, b⟩
b : β
h_b : s b
h_b_in_T : ⟨b, h_b⟩ ∈ T
h2 : a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨b, h_b⟩
⊢ a ∈ f ⟨b, h_b⟩

Tactic:
revert h2

Result:
case intro.intro.intro.refine_1.h.mpr
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : a_1 ∈ s), ⟨a_1, b⟩ ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨a_1, b⟩
b : β
h_b : s b
h_b_in_T : ⟨b, h_b⟩ ∈ T
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑⟨b, h_b⟩ → a ∈ f ⟨b, h_b⟩

Proof state:
case h
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)
x : Set α
⊢ (∃ a, s a ∧ x ∈ g a) ↔ ∃ i ∈ s, x ∈ g i

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)
⊢ ∃ T f, ↑T ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
have : t ∈ generatePiSystem (⋃ b : Subtype s, (g ∘ Subtype.val) b) := by
  suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b by rwa [h1]
  ext x
  simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists, Subtype.coe_mk]
  rfl

Result:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ b ∈ s, g b)
this : t ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
⊢ ∃ T f, ↑T ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Proof state:
case intro.intro.intro.refine_2.intro.a
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : ⟨b, ⋯⟩ ∈ T
h_b_alt : b = ↑⟨b, h_b_w⟩
⊢ ⟨b, h_b_w⟩ ∈ T

Tactic:
apply h_b_h

Result:
no goals