no goals
α : Type u_1
β : Type ?u.162516
β₂ : Type ?u.162519
γ : Type ?u.162522
ι : Sort ?u.162525
ι' : Sort ?u.162528
κ : ι → Sort ?u.162533
κ' : ι' → Sort ?u.162538
inst✝ : CompleteLattice α
f g s t : ι → α
a b x y : α
⊢ x ⊔ y = ⨆ (b : Bool), bif b then x else y
rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]