α : Type u_1
β : Type u_2
β₂ : Type ?u.63820
γ : Type ?u.63823
ι : Sort u_3
ι' : Sort ?u.63829
κ : ι → Sort ?u.63834
κ' : ι' → Sort ?u.63839
inst✝ : SupSet α
f✝ g✝ : ι → α
g : β → α
f : ι → β
⊢ sSup (range (g ∘ f)) = sSup (range fun i => g (f i))
α : Type u_1
β : Type u_2
β₂ : Type ?u.63820
γ : Type ?u.63823
ι : Sort u_3
ι' : Sort ?u.63829
κ : ι → Sort ?u.63834
κ' : ι' → Sort ?u.63839
inst✝ : SupSet α
f✝ g✝ : ι → α
g : β → α
f : ι → β
⊢ (⨆ (b : ↑(range f)), g ↑b) = ⨆ (i : ι), g (f i)
rw [iSup, iSup, ← image_eq_range, ← range_comp]
no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.63820
γ : Type ?u.63823
ι : Sort u_3
ι' : Sort ?u.63829
κ : ι → Sort ?u.63834
κ' : ι' → Sort ?u.63839
inst✝ : SupSet α
f✝ g✝ : ι → α
g : β → α
f : ι → β
⊢ sSup (range (g ∘ f)) = sSup (range fun i => g (f i))
rfl