no goals
α : Type u_3
β : Type u_2
β₂ : Type ?u.164848
γ : Type ?u.164851
ι : Sort ?u.164854
ι' : Sort ?u.164857
κ : ι → Sort ?u.164862
κ' : ι' → Sort ?u.164867
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
p : β → Type u_1
f : Sigma p → α
c : α
⊢ (⨆ (x : Sigma p), f x) ≤ c ↔ (⨆ (i : β) (j : p i), f { fst := i, snd := j }) ≤ c
simp only [iSup_le_iff, Sigma.forall]