simps and function application

Stream: general

[Simon Hudon]

I'm creating instances for a bundled hom type:

import order.preorder_hom
import order.lattice

variables {α β : Type*} [preorder α]

@[simps {rhs_md := semireducible}]
instance [partial_order β] : partial_order (α →ₘ β) :=
partial_order.lift preorder_hom.to_fun $ by rintro ⟨⟩ ⟨⟩ h; congr; exact h


@[simps]
instance [semilattice_sup β] : semilattice_sup (α →ₘ β) :=
{ sup := λ f g, ⟨f.to_fun ⊔ g.to_fun, λ x y h, sup_le_sup (f.monotone h) (g.monotone h)⟩,
  le_sup_left := λ a b x, le_sup_left,
  le_sup_right := λ a b x, le_sup_right,
  sup_le := λ a b c h₀ h₁ x, sup_le (h₀ x) (h₁ x),
  .. (_ : partial_order (α →ₘ β)) }

-- generates
-- preorder_hom.semilattice_sup_sup_to_fun : ∀ {α : Type u_1} [_inst_1 : preorder α] {β : Type u_2}
-- [_inst_4 : semilattice_sup β] (f g : α →ₘ β) (a : α),
-- ⇑(semilattice_sup.sup f g) a = (f.to_fun ⊔ g.to_fun) a

simps generates the wrong equality for sup. I'd like it to generate ⇑(semilattice_sup.sup f g) a = f a ⊔ g a. Is this possible and if so how?

[Simon Hudon]

Update: Defining sup as:

sup := λ f g, ⟨λ a, f a ⊔ g a, λ x y h, sup_le_sup (f.monotone h) (g.monotone h)⟩,

does it but why does simps not know that we can distribute function application and sup on pi types?

[Johan Commelin]

@Floris van Doorn Do you think simps could be made to take here of https://github.com/leanprover-community/mathlib/pull/4125#discussion_r487682684?