## Stream: general

### Topic: simps and function application

#### Simon Hudon (Sep 04 2020 at 16:26):

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 (Sep 04 2020 at 16:28):

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 (Sep 14 2020 at 08:02):

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

Last updated: May 10 2021 at 00:31 UTC