α : Type u_2
β : Type ?u.59227
γ : Type ?u.59230
ι : Sort u_1
inst✝¹ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
inst✝ : Unique ι
s : ι → α
this : ∀ (i : ι), s i = s default
⊢ (⨆ (i : ι), s i) = s default
α : Type u_2
β : Type ?u.59227
γ : Type ?u.59230
ι : Sort u_1
inst✝¹ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
inst✝ : Unique ι
s : ι → α
⊢ (⨆ (i : ι), s i) = s default
have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)
no goals
α : Type u_2
β : Type ?u.59227
γ : Type ?u.59230
ι : Sort u_1
inst✝¹ : ConditionallyCompleteLattice α
s✝ t : Set α
a b : α
inst✝ : Unique ι
s : ι → α
this : ∀ (i : ι), s i = s default
⊢ (⨆ (i : ι), s i) = s default
simp only [this, ciSup_const]