Inverse image and cast to subsets

Stream: new members

[Michael Rothgang]

I'm stuck trying to prove a statement about preimages, involving casting of subsets. Mathematically, roughly my problem is: if $s\subset t$ are subsets of $X$ and I'm given an element $x\in t$, how can I, in Lean, obtain $x$ as an element of $s$? Find a MWE below. (I guess solving one direction might already help for the other one.)

import Mathlib.Topology.Basic
open Topology

lemma minimized {X Y Z: Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : Y → Z} {g : X → Y} {t: Set X} {u: Set Y}
    {x : X} (ht: t ∈ 𝓝 x) (hu: u ∈ 𝓝 (g x)) : True /- dummy statement -/ := by
  -- idea: shrink u to g(t); more precisely: restrict g to the preimage of u under g':=g∣t.
  let g' := t.restrict g
  let t' : Set X := ↑(g' ⁻¹' u)
  -- The following is mathematically easy; I'm wrestling with filling the sorries.
  have h₁ : t' = t ∩ g ⁻¹' u := by
    apply Iff.mpr (Set.Subset.antisymm_iff)
    constructor
    · intro x hx
      constructor
      · exact Set.coe_subset hx
      · -- goal: x ∈ g ⁻¹' u
        -- informal argument: as x ∈ t', we can apply g' (and land in u by definition), so g'(x)=g(x) ∈ u
        -- my first step: present x is an element of t
        have : x ∈ t := by sorry -- apply Set.mem_coe_of_mem hx, somehow?
        -- now I'm stuck
        sorry
    · rintro x ⟨ht, hgu⟩
      -- goal: x ∈ t'
      -- informal argument: as x ∈ t, we can write g(x)=g'(x); the rhs lies in u, so x ∈ g⁻¹(u) also
      sorry
  trivial

[Alex J. Best]

Instead of thinking about your problem I just hit it with a hammer and it worked :wink:

import Mathlib.Topology.Basic
open Topology

lemma minimized {X Y Z: Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : Y → Z} {g : X → Y} {t: Set X} {u: Set Y}
    {x : X} (ht: t ∈ 𝓝 x) (hu: u ∈ 𝓝 (g x)) : True /- dummy statement -/ := by
  -- idea: shrink u to g(t); more precisely: restrict g to the preimage of u under g':=g∣t.
  let g' := t.restrict g
  set t' : Set X := ↑(g' ⁻¹' u) with ht'
  -- The following is mathematically easy; I'm wrestling with filling the sorries.
  have h₁ : t' = t ∩ g ⁻¹' u := by
    rw [ht']
    ext1 y
    simp [Lean.Internal.coeM]
    aesop

  trivial

[Alex J. Best]

I've seen this Lean.Internal.coeM thing showing up before and it probably shouldn't show up in mathematical proofs, but it seems to be unavoidable now :confused:

[Ruben Van de Velde]

Yeah, I was worried about that coeM too, so I avoided it:

import Mathlib.Topology.Basic
open Topology

lemma minimized {X Y Z: Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : Y → Z} {g : X → Y} {t: Set X} {u: Set Y}
    {x : X} (ht: t ∈ 𝓝 x) (hu: u ∈ 𝓝 (g x)) : True /- dummy statement -/ := by
  -- idea: shrink u to g(t); more precisely: restrict g to the preimage of u under g':=g∣t.
  let g' := t.restrict g
  let t'' := (g' ⁻¹' u)
  let t' : Set X := { (x : X) | x ∈ t'' }
  -- The following is mathematically easy; I'm wrestling with filling the sorries.
  have h₁ : t' = t ∩ g ⁻¹' u := by
    apply Iff.mpr (Set.Subset.antisymm_iff)
    constructor
    · intro x hx
      simp at hx
      obtain ⟨x, ha1, ha2, rfl⟩ := hx
      constructor
      · assumption
      · -- goal: x ∈ g ⁻¹' u
        -- informal argument: as x ∈ t', we can apply g' (and land in u by definition), so g'(x)=g(x) ∈ u
        -- my first step: present x is an element of t
        -- now I'm stuck
        simp [ha1]
    · rintro x ⟨ht, hgu⟩
      -- goal: x ∈ t'
      -- informal argument: as x ∈ t, we can write g(x)=g'(x); the rhs lies in u, so x ∈ g⁻¹(u) also
      simp at hgu
      simp
      use x
  trivial

[Michael Rothgang]

Wow, thanks a lot for the quick responses, both of you!

[Michael Rothgang]

I didn't know about set (or ext1) before.
And I'm glad to have an aesop-free argument in case I need one (the aesop output is not nice).

[Jireh Loreaux]

docs#Lean.Internal.coeM is just the coercion between monadic types induced by a coercion between their underlying types. It's not a problem that we see it, just a bit annoying. We need to find a good place to add the @[coe] attribute to this declaration. This is in core, but the attribute isn't declared until Std.

[Jireh Loreaux]

In your case, Set is the monad.

[Jireh Loreaux]

For example, if t : Set X, then there is a coercion (↑) : ↥t → X (this is Subtype.val), and then Lean.Interal.coeM is the coercion (↑) : Set ↥t → Set X, but it doesn't get the ↑ because it doesn't have the @[coe] attribute.

[Alex J. Best]

Jireh Loreaux said:

docs#Lean.Internal.coeM is just the coercion between monadic types induced by a coercion between their underlying types. It's not a problem that we see it, just a bit annoying. We need to find a good place to add the @[coe] attribute to this declaration. This is in core, but the attribute isn't declared until Std.

I'm not sure Jireh, the docstring of Lean.Internal.coeM quite clearly says "Helper definition used by the elaborator. It is not meant to be used directly by users." which makes me worry that something is not quite working as intended here

[Jireh Loreaux]

I think that docstring still agrees with what I said. The user should never write down this function, it should only exist as the result of other coercions.

[Alex J. Best]

I'm still unconvinced, it's tagged as @[coe_decl] which says, "auxiliary definition used to implement coercion (unfolded during elaboration" but I've not yet finished debugging why the unfolding is not working in this case

[Alex J. Best]

With https://github.com/alexjbest/lean4/tree/patch-4

import Mathlib.Data.Set.Functor
example {A : Type} {B : Set A} {C : Set B} : (C : Set A) = B := by
  sorry

gives a goal

(do
    let a ← C
    pure ↑a) =
  B

instead of Internal.coeM C = B, one advantage of this is that dsimp now results in something sensible ⋃ (i : ↑B) (_ : i ∈ C), {↑i} = B

[Anatole Dedecker]

I agree that this is cleaner. I really think we shouldn't train users to see names such as Internal.something as things that should be used in everyday proofs. Am I right that there was no coercion form Set A to Set B given a coercion from A to B in Lean3? Is there any risk of such a coercion causing diamonds somewhere?

[Yaël Dillies]

There was no such coercion, no. I don't think such a coercion will cause a diamond, unless we also introduce the Coe A B → Coe (Set B) (Set A) instance given by the preimage, in which case they'll conflict when A = B.