no goals
α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : Has (generate s) t₁
ht₂ : Has (generate s) t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this✝¹ : Has (generate s) s₁
this✝ : generate s ≤ restrictOn (generate s) this✝¹
this : Has (generate s) (t₂ ∩ s₁)
⊢ Has (generate s) (s₁ ∩ t₂)
rwa [inter_comm]