no goals
α : Type u_2
β : Type u_1
γ : Type ?u.539269
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset β
t : Finset α
f : α → Finset β
⊢ _root_.Disjoint s (Finset.biUnion t f) ↔ ∀ (i : α), i ∈ t → _root_.Disjoint s (f i)
simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s