α : Type u_2
β : Type ?u.102985
β₂ : Type ?u.102988
γ : Type ?u.102991
ι : Sort u_1
ι' : Sort ?u.102997
κ : ι → Sort ?u.103002
κ' : ι' → Sort ?u.103007
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ (i : ι) (h : p i), f i h) ⊔ a = ⨆ (i : ι) (h : p i), f i h ⊔ a
α : Type u_2
β : Type ?u.102985
β₂ : Type ?u.102988
γ : Type ?u.102991
ι : Sort u_1
ι' : Sort ?u.102997
κ : ι → Sort ?u.103002
κ' : ι' → Sort ?u.103007
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ (⨆ (i : ι) (h : p i), f i h) ⊔ a = ⨆ (i : ι) (h : p i), f i h ⊔ a
haveI : Nonempty { i // p i } :=
    let ⟨i, hi⟩ := h
    ⟨⟨i, hi⟩⟩
no goals
α : Type u_2
β : Type ?u.102985
β₂ : Type ?u.102988
γ : Type ?u.102991
ι : Sort u_1
ι' : Sort ?u.102997
κ : ι → Sort ?u.103002
κ' : ι' → Sort ?u.103007
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ (i : ι) (h : p i), f i h) ⊔ a = ⨆ (i : ι) (h : p i), f i h ⊔ a
rw [iSup_subtype', iSup_subtype', iSup_sup]