no goals
F : Type u_2
α : Type u_3
β : Type u_1
γ : Type ?u.109238
ι : Type u_4
κ : Type ?u.109244
inst✝⁴ : SemilatticeInf α
inst✝³ : OrderTop α
s✝¹ s₁ s₂ : Finset β
f✝ g✝ : β → α
a : α
inst✝² : SemilatticeInf β
inst✝¹ : OrderTop β
inst✝ : InfTopHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : ↑f (inf s g) = inf s (↑f ∘ g)
⊢ ↑f (inf (cons i s x✝) g) = inf (cons i s x✝) (↑f ∘ g)
rw [inf_cons, inf_cons, map_inf, h, Function.comp_apply]