no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.111002
γ : Type ?u.111005
ι : Sort u_3
ι' : Sort ?u.111011
κ : ι → Sort ?u.111016
κ' : ι' → Sort ?u.111021
inst✝ : CompleteLattice α
f✝ g✝ s t : ι → α
a b : α
g : β → α
f : ι → β
⊢ (⨆ (b : β) (_ : b ∈ range f), g b) = ⨆ (i : ι), g (f i)
rw [← iSup_subtype'', iSup_range']