-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
hst_nonempty : ((↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂).Nonempty
let let₁ let₂ let₃ : (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₄ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₅ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₆ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  let t₂' := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ)
    (h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₇ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  let t₂' := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ)
    (h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i) (h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ),
    (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C
let₈ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  let t₂' := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ)
    (h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i) (h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ),
    (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ squareCylinders (α := α) C
refine_1 :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  let t₂' := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ)
    (h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i) (h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ),
    (fun (i : ι) ↦ t₁' i ∩ t₂' i) ∈ Set.pi (α := fun (i : ι) ↦ Set (α i)) univ C
refine_2 refine_2₁ :
  let t₁' := s₁.piecewise (π := fun (i : ι) ↦ Set (α i)) t₁ fun (i : ι) ↦ univ;
  let t₂' := s₂.piecewise (π := fun (i : ι) ↦ Set (α i)) t₂ fun (i : ι) ↦ univ;
  ∀ (h1 : ∀ i ∈ (↑s₁ : Set ι), t₁ i = t₁' i) (h1' : ∀ i ∉ (↑s₁ : Set ι), t₁' i = univ)
    (h2 : ∀ i ∈ (↑s₂ : Set ι), t₂ i = t₂' i) (h2' : ∀ i ∉ (↑s₂ : Set ι), t₂' i = univ),
    Eq (α := Set ((i : ι) → α i)) (((↑s₁ : Set ι) ∪ (↑s₂ : Set ι)).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i)
      ((↑(s₁ ∪ s₂) : Set ι).pi (α := α) fun (i : ι) ↦ t₁' i ∩ t₂' i)
⊢ (↑s₁ : Set ι).pi (α := α) t₁ ∩ (↑s₂ : Set ι).pi (α := α) t₂ ∈ squareCylinders (α := α) C

Tactic:
classical
  let t₁' := s₁.piecewise t₁ (fun i ↦ univ)
  let t₂' := s₂.piecewise t₂ (fun i ↦ univ)
  have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
  have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ :=
    fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
  rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
  refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
  · rw [mem_univ_pi]
    intro i
    have : (t₁' i ∩ t₂' i).Nonempty := by
      obtain ⟨f, hf⟩ := hst_nonempty
      rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf
      refine ⟨f i, ⟨?_, ?_⟩⟩
      · by_cases hi₁ : i ∈ s₁
        · exact hf.1 i hi₁
        · rw [h1' i hi₁]
          exact mem_univ _
      · by_cases hi₂ : i ∈ s₂
        · exact hf.2 i hi₂
        · rw [h2' i hi₂]
          exact mem_univ _
    refine hC i _ ?_ _ ?_ this
    · by_cases hi₁ : i ∈ s₁
      · rw [← h1 i hi₁]
        exact h₁ i (mem_univ _)
      · rw [h1' i hi₁]
        exact hC_univ i
    · by_cases hi₂ : i ∈ s₂
      · rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)
      · rw [h2' i hi₂]
        exact hC_univ i
  · rw [Finset.coe_union]

Premises used: Set.mem_univ_pi, Finset.coe_union