no goals
F : Type ?u.157856
α : Type u_1
β : Type ?u.157862
γ : Type ?u.157865
ι : Type u_2
κ : Type ?u.157871
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
a : α
⊢ _root_.Disjoint (sup s f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → _root_.Disjoint (f i) a
simp only [disjoint_iff, sup_inf_distrib_right, Finset.sup_eq_bot_iff]