If U ⊆ V, then f ⁻¹(U) ⊆ f ⁻¹(V): three questions

Stream: new members

[Mitchell Lee]

Here's a simple theorem:

example {X Y : Type*} {U V : Set Y} (h : U ⊆ V) (f : X → Y) : f ⁻¹' U ⊆ f ⁻¹' V :=
  fun _ hx ↦ h hx

A few questions:

1. Is this in mathlib?

2. If I try to simplify the proof to fun _ ↦ h, I get the message

type mismatch
  h
has type
  U ⊆ V : Prop
but is expected to have type
  x✝ ∈ f ⁻¹' U → x✝ ∈ f ⁻¹' V : Prop.

Why doesn't this work?

3. If I try to prove the theorem using by exact?, it suggests by exact fun ⦃a⦄ ↦ h. This doesn't work for the same reason as fun _ ↦ h doesn't. Is exact? supposed to be able to suggest an incorrect proof?

[Shanghe Chen]

Hi for 1. I searched https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Image.html#Set.preimage_mono with loogle https://loogle.lean-lang.org/?q=%7C-+_+%E2%81%BB%C2%B9%27+_+%E2%8A%86+_+%E2%81%BB%C2%B9%27+_

[Mitchell Lee]

Thanks. I wasn't finding it because I was searching for theorems with the words "preimage" and "subset" in the name.

[Luigi Massacci]

Might be wrong, but for 1 note that U ⊆ V := ∀ ⦃a⦄, a ∈ U → a ∈ V, which is not the same as a ∈ U → a ∈ V (for some fixed a). Of course if it works "forall" it works for some instantiating the quantifier, but term mode is dumb and can't infer what to substitute on its own. By comparison, if you go to tactic mode and do the equivalent:

example {X Y : Type*} {U V : Set Y} (h : U ⊆ V) (f : X → Y) : f ⁻¹' U ⊆ f ⁻¹' V := by
  intro _; apply h

it works just fine

[Alex J. Best]

You could also do one of

import Mathlib

example {X Y : Type*} {U V : Set Y} (h : U ⊆ V) (f : X → Y) : f ⁻¹' U ⊆ f ⁻¹' V :=
  fun _ ↦ h (a := _)

example {X Y : Type*} {U V : Set Y} (h : U ⊆ V) (f : X → Y) : f ⁻¹' U ⊆ f ⁻¹' V :=
  fun _ ↦ @h _

[Mitchell Lee]

I see. Thanks for the answers. Any insight on the third question? It seems like it might actually be a bug.

[Ruben Van de Velde]

Yeah, I'd think that's a bug as well

[Kevin Buzzard]

I think this was reported a while ago. In general it's best to run exact after you can't do intro any more because it might not get binders right (typeclasses also mess it up if they're right of the colon)