automation for easy set lemma

Stream: mathlib4

[Kevin Buzzard]

I am not very good at automation. The below lemma just came up in FLT and somehow I feel like it should be a one-liner because I can in some sense prove it without moving my brain and then golf it a bit with defeq abuse etc (which I did below), but are we yet at the stage where we can destroy it in one line? tauto_set didn't do it, neither does aesop or grind, and I still have no feeling as to how to modify things like grind to make them solve this.

import Mathlib

lemma foo {X Y : Type*} {f : X → Y} {U : Set Y} {x : X} (h : f ⁻¹' U = {x}) :
    Set.range f ∩ U = {f x} := by
  apply Set.Subset.antisymm
  · rintro - ⟨⟨c, rfl⟩, hc⟩
    rw [← Set.mem_preimage] at hc
    grind
  · rintro - rfl
    constructor
    · simp
    · simp [← Set.mem_preimage, h]

[Yakov Pechersky]

Unpolished attempt:

import Mathlib

lemma foo {X Y : Type*} {f : X → Y} {U : Set Y} {x : X} (h : f ⁻¹' U = {x}) :
    Set.range f ∩ U = {f x} := by
  simp [Set.ext_iff] at h
  ext
  grind

[Rémy Degenne]

An application of the method ext; simp; grind for set equality goals works.

import Mathlib

lemma foo {X Y : Type*} {f : X → Y} {U : Set Y} {x : X} (h : f ⁻¹' U = {x}) :
    Set.range f ∩ U = {f x} := by
  ext y
  rw [Set.ext_iff] at h
  simp at h ⊢
  grind

I have to ext and simp at h as well as the goal though.

[Yakov Pechersky]

Basically, any time you have concrete sets like a singleton, using ext or the equivalent lemma will lead to better hypotheses that work with implications.

[Yakov Pechersky]

Feature suggestion, ext at h

[Damiano Testa]

By the way, this also works (exploiting the same tricks as above):

attribute [simp] Set.ext_iff

lemma foo {X Y : Type*} {f : X → Y} {U : Set Y} {x : X} (h : f ⁻¹' U = {x}) :
    Set.range f ∩ U = {f x} := by
  aesop

[Chris Henson]

Yakov Pechersky said:

Unpolished attempt:

import Mathlib

lemma foo {X Y : Type*} {f : X → Y} {U : Set Y} {x : X} (h : f ⁻¹' U = {x}) :
    Set.range f ∩ U = {f x} := by
  simp [Set.ext_iff] at h
  ext
  grind

Note that you can remove the ext here.

[Kevin Buzzard]

Excellent, thanks!

[Artie Khovanov]

Yakov Pechersky said:

Feature suggestion, ext at h

I currently write apply_fun (x \in \.) at h
But automatically finding and applying function congruence with ext lemmas would be cool!

[Martin Dvořák]

Should tauto_set be extended to know about ⁻¹' and similar?