no goals
F : Type u_2
α : Type u_3
β : Type u_1
γ : Type ?u.18510
ι : Type u_4
κ : Type ?u.18516
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
s✝¹ s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : ↑f (sup s g) = sup s (↑f ∘ g)
⊢ ↑f (sup (cons i s x✝) g) = sup (cons i s x✝) (↑f ∘ g)
rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]