no goals
α : Type u_1
β : Type ?u.162120
β₂ : Type ?u.162123
γ : Type ?u.162126
ι : Sort ?u.162129
ι' : Sort ?u.162132
κ : ι → Sort ?u.162137
κ' : ι' → Sort ?u.162142
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : Bool → α
⊢ (⨆ (b : Bool), f b) = f true ⊔ f false
rw [iSup, Bool.range_eq, sSup_pair, sup_comm]