How do I configure an `equiv` to work with `simps`?

Stream: general

[Scott Morrison]

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]

Do you need something like

initialize_simps_projections homeo (to_fun → apply)

[Eric Wieser]

It looks like ≃ₜ is missing a has_coe_to_fun?

[Eric Wieser]

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]

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

[Johan Commelin]

docs#homeomorph.has_coe_to_fun

[Eric Wieser]

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

[Eric Wieser]

But your suggestion may still work

[Floris van Doorn]

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]

Why don't we make all structures old structures?

[Floris van Doorn]

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]

docs#rel_embedding, and probably everything in that file

[Yury G. Kudryashov]

docs#local_homeomorph