no goals
F : Type ?u.63465
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Type ?u.63477
κ : Type ?u.63480
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : ¬c ∈ t
ih : g (sup t f) = sup t (g ∘ f)
⊢ g (sup (cons c t hc) f) = sup (cons c t hc) (g ∘ f)
rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]