no goals
α : Type u_3
β : Type u_1
β₂ : Type ?u.168938
γ : Type u_2
ι : Sort ?u.168944
ι' : Sort ?u.168947
κ : ι → Sort ?u.168952
κ' : ι' → Sort ?u.168957
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β ⊕ γ → α
c : α
⊢ (⨆ (x : β ⊕ γ), f x) ≤ c ↔ ((⨆ (i : β), f (Sum.inl i)) ⊔ ⨆ (j : γ), f (Sum.inr j)) ≤ c
simp only [sup_le_iff, iSup_le_iff, Sum.forall]