## Stream: general

### Topic: How do I configure an equiv to work with simps?

#### Scott Morrison (Apr 06 2021 at 09:40):

For example, in

import topology.instances.real
import topology.algebra.group_with_zero

noncomputable theory

/-- The map λ x, a * x + b, as a homeomorphism from ℝ to itself, when a ≠ 0. -/
@[simps?]
def affine_homeo (a b : ℝ) (h : a ≠ 0) : ℝ ≃ₜ ℝ :=
{ to_fun := λ x, a * x + b,
inv_fun := λ y, (y - b) / a,
left_inv := λ x, by { simp only [add_sub_cancel], exact mul_div_cancel_left x h, },
right_inv := λ y, by { simp [mul_div_cancel' _ h], }, }


@[simps] doesn't generate the lemmas I want: they look like

[simps] > adding projection affine_homeo_to_equiv_apply:
> ∀ (a b : ℝ) (h : a ≠ 0) (x : ℝ), ⇑((affine_homeo a b h).to_equiv) x = a * x + b


whereas I'd prefer just

@[simp] lemma affine_homeo_apply (a b : ℝ) (h : a ≠ 0) (x : ℝ) :
affine_homeo a b h x = a * x + b := rfl


Is there some magic incantation that will cause simps to do this in the first place? @Floris van Doorn?

#### Johan Commelin (Apr 06 2021 at 09:44):

Do you need something like

initialize_simps_projections homeo (to_fun → apply)


#### Eric Wieser (Apr 06 2021 at 09:45):

It looks like ≃ₜ  is missing a has_coe_to_fun?

#### Eric Wieser (Apr 06 2021 at 09:46):

https://leanprover-community.github.io/mathlib_docs/notes.html#function%20coercion may be relevant. I don't know what ≃ₜ is so can't look at the docs for it

#### Johan Commelin (Apr 06 2021 at 09:47):

I think it's homeomorph (test: docs#homeomorph)

#### Johan Commelin (Apr 06 2021 at 09:48):

docs#homeomorph.has_coe_to_fun

#### Eric Wieser (Apr 06 2021 at 09:50):

I think this is because homeomorph is not an old_structure_cmd like the other equivs

#### Eric Wieser (Apr 06 2021 at 09:51):

But your suggestion may still work

#### Floris van Doorn (Apr 06 2021 at 15:46):

This is unfortunately not supported yet.
As Eric said, the reason is that homeomorph is not an old_structure_cmd, so therefore, there is no single projection homeomorph a b -> (a -> b). Therefore, to support this, simps would have to look at a composition of projections and a custom projection for that. That is not supported yet, but it is at the top of the list of #5489. I'll see if I can implement it soon(ish).

#### Kevin Buzzard (Apr 06 2021 at 16:03):

Why don't we make all structures old structures?

#### Floris van Doorn (Apr 07 2021 at 03:30):

This is implemented in #7074.
still have to test it in some examples of mathlib.

Are there other structures like homeomorph that extend a structure without old_structure_cmd and that have a coercion to functions?

#### Eric Wieser (Apr 07 2021 at 07:09):

docs#rel_embedding, and probably everything in that file

#### Yury G. Kudryashov (Apr 09 2021 at 00:39):

docs#local_homeomorph

Last updated: Dec 20 2023 at 11:08 UTC