no goals
F : Type ?u.92388
α : Type u_2
β : Type u_1
γ : Type ?u.92397
ι : Type ?u.92400
κ : Type ?u.92403
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ sup s f = sSup (f '' ↑s)
classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.comp.left_id]
no goals
F : Type ?u.92388
α : Type u_2
β : Type u_1
γ : Type ?u.92397
ι : Type ?u.92400
κ : Type ?u.92403
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ sup s f = sSup (f '' ↑s)
rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.comp.left_id]