image is univ implies surjective

Stream: Is there code for X?

[Alex Kontorovich]

I'm surprised there's no one-liner closing this? (If a function's image is univ, then the function is Surjective.)

import Mathlib

example {X Y : Type*} (f : X → Y) (hf : f '' univ = univ) : Function.Surjective f := by
  sorry
-- exact? fails
-- simp? fails
-- apply? junk
-- rw? junk

Thanks!

[Jireh Loreaux]

We have docs#Set.range_iff_surjective

[Riccardo Brasca]

I don't understand why simp is not firing. We have docs#Set.image_univ

[Jireh Loreaux]

import Mathlib

example {X Y : Type*} (f : X → Y) (hf : f '' univ = univ) : Function.Surjective f := by
    Set.range_iff_surjective.mp (image_univ ▸ hf)

[Riccardo Brasca]

Because I forgot at hf

[Riccardo Brasca]

example {X Y : Type*} (f : X → Y) (hf : f '' univ = univ) : Function.Surjective f := by
  simp at hf
  exact?

works, and from here it's easy to find Jireh's proof.

[Alex Kontorovich]

Ah! So I needed to simp at hf first. I wouldn't have thought of that...

[Alex Kontorovich]

(Is there a yoga for why that would help?)

[Jireh Loreaux]

The thing to realize is that f '' univ is not the canonical spelling, it's Set.range f.

[Riccardo Brasca]

The idea is f '' univ is a strange way of writing the image

[Riccardo Brasca]

I would start your standard list of tactics with simp_all,

simp_all
-- exact? works
-- simp? fails
-- apply? junk
-- rw? junk

[Riccardo Brasca]

Note that if simp does something, it is almost always a good thing, since a lot of results are written using the simp normal form (exactly as in this case)

[Kevin Buzzard]

Yeah, simp normal form is a nice concept to be on top of (and I wasn't on top of it for years). If your hypothesis isn't in simp normal form then it's difficult to use, because there might only be one lemma about it in the whole library, namely the simp lemma turning the hypothesis into its simp normal form where suddenly there are many lemmas which now apply :-)

[Alex Kontorovich]

Great, that's exactly what I was hoping to learn. simp_all instead of just simp. Love it!