-- Module: Mathlib.MeasureTheory.PiSystem
Goal:
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
t : Set α
h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) t
have : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
have₁ :
  ∀ (this : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t),
    ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have₂ : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t
have₃ have₄ :
  ∀ (this : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b)) t),
    ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b
have₅ :
  ∀ (T : Finset (Subtype s)) (f : Subtype s → Set α) (h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val (p := s)) b)
    (h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) (⋂ b ∈ T, f b))
    (this :
      Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b))
        (⋂ b ∈ T, f b)),
    ∃ (T_1 : Finset β) (f_1 : β → Set α),
      (↑T_1 : Set β) ⊆ s ∧ Eq.{u_3 + 1} (α := Set α) (⋂ b ∈ T, f b) (⋂ b ∈ T_1, f_1 b) ∧ ∀ b ∈ T_1, f_1 b ∈ g b
refine_1 :
  ∀ (T : Finset (Subtype s)) (f : Subtype s → Set α) (h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val (p := s)) b)
    (h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) (⋂ b ∈ T, f b))
    (this :
      Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b))
        (⋂ b ∈ T, f b)),
    Eq.{u_3 + 1} (α := Set α) (⋂ b ∈ T, f b)
      (⋂ (b : β),
        ⋂ (_ : Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b),
          Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b)
refine_2 refine_2₁ :
  ∀ (T : Finset (Subtype s)) (f : Subtype s → Set α) (h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val (p := s)) b)
    (h_t : Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ b ∈ s, g b)) (⋂ b ∈ T, f b))
    (this :
      Membership.mem (γ := Set (Set α)) (generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val (p := s)) b))
        (⋂ b ∈ T, f b))
    (b : β),
    Membership.mem (γ := Finset β) (Finset.image (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) T) b →
      Function.extend (fun (x : (↑s : Type u_4)) ↦ (↑x : β)) f (fun (x : β) ↦ ∅) b ∈ g b
⊢ ∃ (T : Finset β) (f : β → Set α), (↑T : Set β) ⊆ s ∧ t = ⋂ b ∈ T, f b ∧ ∀ b ∈ T, f b ∈ g b

Tactic:
classical
  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]
    rfl
  rcases @mem_generatePiSystem_iUnion_elim α (Subtype s) (g ∘ Subtype.val)
      (fun b => h_pi b.val b.property) t this with
    ⟨T, ⟨f, ⟨rfl, h_t'⟩⟩⟩
  refine
    ⟨T.image (fun x : s => (x : β)),
      Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, ?_, ?_⟩
  · ext a
    constructor <;>
      · simp -proj only
          [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
        intro h1 b h_b h_b_in_T
        have h2 := h1 b h_b h_b_in_T
        revert h2
        rw [Subtype.val_injective.extend_apply]
        apply id
  · intro b h_b
    simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
      at h_b
    obtain ⟨h_b_w, h_b_h⟩ := h_b
    have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
    rw [h_b_alt, Subtype.val_injective.extend_apply]
    apply h_t'
    apply h_b_h

Premises used: Finset.set_biInter_finset_image, Finset.mem_image, Subtype.val_injective, Subtype.exists, exists_eq_right, id, Subtype.forall, exists_and_right, Function.Injective.extend_apply, Set.mem_iInter, rfl