Use of Set.preimage_iterate_eq

Stream: general

[Damien Thomine]

I have had some issues with the lemma Set.preimage_iterate_eq

 @[simp]
theorem preimage_iterate_eq {f : α → α} {n : ℕ} :
Set.preimage f^[n] = (Set.preimage f)^[n] := [...]

and more precisely the fact that it has a simp tag. I don't understand the rationale behind this tag, and this lemma complicates everything I do ; but maybe I don't have the right approach.

Basically, the kind of situation which I encounter repeatedly is the following :

• I have a subset U with a complicated expression. I want to prove e.g. that it is open.

• after straightforward manipulations, it can be written as f^[n]^{-1} V for some continuous function f and open subset V. Ideally, a single application of simp suffices.

• conclude using Continuous.iterate and IsOpen.preimage.

The lemma Set.preimage_iterate_eq throws a wrench in this strategy, since it will modify f^[n]^{-1} V to something else. As a result, my current project has too many occurences of simp [-Set.preimage_iterate_eq]. Maybe I could add a new lemma if it were only about continuity, but this is not the only situation where I encounter this difficulty. How can I resolve this obstacle ?

[Scott Morrison]

Have you tried compiling mathlib with the @[simp] removed? If it's not actually used much, possibly we can just remove it.

[Oliver Nash]

IIRC I added that lemma and its simp tag and I think we could just remove the simp attribute. Alternatively you can try adding:

attribute [-simp] Set.preimage_iterate_eq

at the top of your file.

[Yaël Dillies]

It might also mean that you're missing other simp lemmas.

[Damien Thomine]

Thank you for your answer!

Apparently, mathlib compiles just fine when the [simp] attribute on this lemma is removed. Since there is no deeper purpose to this, I'll just do a PR to remove it.

[Eric Wieser]

Should the lemma be stated in the reverse direction?

[Scott Morrison]

(But feel free to ignore this suggestion: if all you care about is removing the simp attribute, that's a fine PR. The fact that there are further changes that would ideally be made is (should not be!) not an obstacle to the simple PR.)