-- Lean 4 proof step from Mathlib.MeasureTheory.PiSystem (goal)
Goal:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
rintro :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    t1 ∩ t2 ∈ piiUnionInter π S
rintro₁ :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
rintro₂ :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
rintro₃ :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty)
    (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S),
    ∃ (t : Finset ι) (_ : (↑t : Set ι) ⊆ S) (f : ι → Set α) (_ : ∀ x ∈ t, f x ∈ π x), t1 ∩ t2 = ⋂ x ∈ t, f x
h :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    let g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ;
    ∀ (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S), ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
h₁ :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    let g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ;
    ∀ (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S) (h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i),
      ∃ (_ : ∀ x ∈ p1 ∪ p2, g x ∈ π x), t1 ∩ t2 = ⋂ x ∈ p1 ∪ p2, g x
h₂ :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    let g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ;
    ∀ (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ S) (h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i) (n : ι) (hn : n ∈ p1 ∪ p2),
      g n ∈ π n
h₃ :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    let g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ;
    ∀ (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ 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
pos :
  ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
    (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
    (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
    let g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ;
    ∀ (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ 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
⊢ IsPiSystem (piiUnionInter π S)
have neg : ∀ (t1 : Set α) (p1 : Finset ι) (hp1S : (↑p1 : Set ι) ⊆ S) (f1 : ι → Set α) (hf1m : ∀ x ∈ p1, f1 x ∈ π x)
  (ht1_eq : t1 = ⋂ x ∈ p1, f1 x) (t2 : Set α) (p2 : Finset ι) (hp2S : (↑p2 : Set ι) ⊆ S) (f2 : ι → Set α)
  (hf2m : ∀ x ∈ p2, f2 x ∈ π x) (ht2_eq : t2 = ⋂ x ∈ p2, f2 x) (h_nonempty : (t1 ∩ t2).Nonempty),
  let g : (n : ι) → Set α := fun (n : ι) ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ;
  ∀ (hp_union_ss : (↑(p1 ∪ p2) : Set ι) ⊆ 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
Tactic: classical
  rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
  simp_rw [piiUnionInter, Set.mem_setOf_eq]
  let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
  have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
    simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
  use p1 ∪ p2, hp_union_ss, g
  have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i := by
    rw [ht1_eq, ht2_eq]
    simp_rw [← Set.inf_eq_inter]
    ext1 x
    simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
    grind
  refine ⟨fun n hn => ?_, h_inter_eq⟩
  simp only [g]
  split_ifs with hn1 hn2 h
  · refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
    rw [h_inter_eq] at h_nonempty
    suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from
      (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
    refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
    refine Set.iInter_subset_of_subset hn ?_
    grind
  · simp [hf1m n hn1]
  · simp [hf2m n h]
  · exact absurd hn (by simp [hn1, h])