Lattice.toSemilatticeSup confusion

Stream: mathlib4

[Moritz Firsching]

I'm trying to prove the following:

import Mathlib

variable {α β ι : Type*} [SemilatticeSup α] [OrderBot α] {s : Finset ι} {f : ι → α} {a : α}

theorem comp_sup_eq_sup_comp_of_nonempty  [LinearOrder α] [SemilatticeSup β] [OrderBot β]
    (g : α → β) (mono_g : Monotone g) (hs : s.Nonempty) : g (s.sup f) = s.sup (g ∘ f) := by
  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs]
  exact Finset.comp_sup'_eq_sup'_comp hs g (fun x y ↦ Monotone.map_sup mono_g x y)

This gives the following error:

type mismatch
  Monotone.map_sup mono_g x y
has type
  g (@max α (@SemilatticeSup.toMax α Lattice.toSemilatticeSup) x y) = g x ⊔ g y : Prop
but is expected to have type
  g (@max α (@SemilatticeSup.toMax α inst✝⁴) x y) = g x ⊔ g y : Prop

where inst✝⁴ has type SemilatticeSup α.
What is going on here, and how can I make it work?
Context is shortening a proof where a more specific version of this theorem is needed: #17553.

[Daniel Weber]

You have a diamond — there's a semilatticesup both directly and from the linear order. You can remove the semilatticesup instance

[Moritz Firsching]

When I remove [SemilatticeSup β], I first get a failure for [OrderBot β], which I can fix by adding [Preorder β], but then s.sup (g ∘ f)complains:

failed to synthesize
  SemilatticeSup β

[Daniel Weber]

Not on \beta, the instance on \alpha

[Moritz Firsching]

perfect, works now, thanks!