no goals
α : Type u_1
β : Type ?u.92752
β₂ : Type ?u.92755
γ : Type ?u.92758
ι : Sort ?u.92761
ι' : Sort ?u.92764
κ : ι → Sort ?u.92769
κ' : ι' → Sort ?u.92774
inst✝¹ : CompleteLattice α
f g s t : ι → α
a✝ b : α
p : Prop
inst✝ : Decidable p
a : p → α
⊢ (⨆ (h : p), a h) = if h : p then a h else ⊥
by_cases h : p <;> simp [h]